Documentation

Lean.Elab.Exception

def Lean.Elab.throwPostpone {m : Type u_1 → Type u_2} {α : Type u_1} [MonadExceptOf Lean.Exception m] :
m α
Equations
Instances For
    def Lean.Elab.throwUnsupportedSyntax {m : Type u_1 → Type u_2} {α : Type u_1} [MonadExceptOf Lean.Exception m] :
    m α
    Equations
    Instances For
      Equations
      Instances For
        Equations
        Instances For
          def Lean.Elab.throwAbortCommand {α : Type u_1} {m : Type u_1 → Type u_2} [MonadExcept Lean.Exception m] :
          m α
          Equations
          Instances For
            def Lean.Elab.throwAbortTerm {α : Type u_1} {m : Type u_1 → Type u_2} [MonadExcept Lean.Exception m] :
            m α
            Equations
            Instances For
              def Lean.Elab.throwAbortTactic {α : Type u_1} {m : Type u_1 → Type u_2} [MonadExcept Lean.Exception m] :
              m α
              Equations
              Instances For
                def Lean.Elab.mkMessageCore (fileName : String) (fileMap : Lean.FileMap) (data : Lean.MessageData) (severity : Lean.MessageSeverity) (pos : String.Pos) (endPos : String.Pos) :
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For