Lean.Elab.BuiltinCommand

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Elab.Command.withNamespace {α : Type} (ns : Lean.Name) (elabFn : Lean.Elab.Command.CommandElabM α) :

Lean.Elab.Command.CommandElabM α

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Elab.Command.elabNamespace:

Lean.Elab.Command.CommandElab

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Elab.Command.elabSection:

Lean.Elab.Command.CommandElab

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Elab.Command.elabNonComputableSection:

Lean.Elab.Command.CommandElab

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Elab.Command.elabEnd:

Lean.Elab.Command.CommandElab

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Elab.Command.elabChoice:

Lean.Elab.Command.CommandElab

Equations

Lean.Elab.Command.elabChoice stx = Lean.Elab.Command.elabChoiceAux (Lean.Syntax.getArgs stx) 0

source

def Lean.Elab.Command.elabUniverse:

Lean.Elab.Command.CommandElab

Equations

Lean.Elab.Command.elabUniverse n = Lean.Syntax.forArgsM (Lean.Syntax.getOp n 1) Lean.Elab.Command.addUnivLevel

source

def Lean.Elab.Command.elabInitQuot:

Lean.Elab.Command.CommandElab

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Elab.Command.elabExport:

Lean.Elab.Command.CommandElab

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Elab.Command.elabOpen:

Lean.Elab.Command.CommandElab

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Elab.Command.elabVariable:

Lean.Elab.Command.CommandElab

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Elab.Command.elabCheckCore (ignoreStuckTC : Bool) :

Lean.Elab.Command.CommandElab

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Elab.Command.elabCheck:

Lean.Elab.Command.CommandElab

Equations

Lean.Elab.Command.elabCheck = Lean.Elab.Command.elabCheckCore true

source

def Lean.Elab.Command.elabReduce:

Lean.Elab.Command.CommandElab

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Elab.Command.hasNoErrorMessages:

Lean.Elab.Command.CommandElabM Bool

Equations

Lean.Elab.Command.hasNoErrorMessages = do let a ← get pure !Lean.MessageLog.hasErrors a.messages

source

def Lean.Elab.Command.failIfSucceeds (x : Lean.Elab.Command.CommandElabM Unit) :

Lean.Elab.Command.CommandElabM Unit

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Elab.Command.elabCheckFailure:

Lean.Elab.Command.CommandElab

Equations

One or more equations did not get rendered due to their size.

source

unsafe def Lean.Elab.Command.elabEvalUnsafe:

Lean.Elab.Command.CommandElab

Equations

One or more equations did not get rendered due to their size.

source

@[implementedBy Lean.Elab.Command.elabEvalUnsafe]

opaque Lean.Elab.Command.elabEval:

Lean.Elab.Command.CommandElab

source

def Lean.Elab.Command.elabSynth:

Lean.Elab.Command.CommandElab

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Elab.Command.elabSetOption:

Lean.Elab.Command.CommandElab

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Elab.Command.expandInCmd:

Lean.Macro

Equations

One or more equations did not get rendered due to their size.