def Lean.Elab.Command.elabModuleDoc : Lean.Elab.Command.CommandElab

Equations

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

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

Equations

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

def Lean.Elab.Command.elabNamespace : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabSection : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabNonComputableSection : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabEnd : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabChoice : Lean.Elab.Command.CommandElab

Equations

• Lean.Elab.Command.elabChoice stx = Lean.Elab.Command.elabChoiceAux stx.getArgs 0

def Lean.Elab.Command.elabUniverse : Lean.Elab.Command.CommandElab

Equations

• Lean.Elab.Command.elabUniverse n = n[1].forArgsM Lean.Elab.Command.addUnivLevel

def Lean.Elab.Command.elabInitQuot : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabExport : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabOpen : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabVariable : Lean.Elab.Command.CommandElab

Equations

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

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

Equations

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

def Lean.Elab.Command.elabCheck : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabReduce : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabReduce.go (tk : Lean.Syntax) (term : Lean.Syntax) (skipProofs : optParam Bool true) (skipTypes : optParam Bool true) : Lean.Elab.Command.CommandElabM Unit

Equations

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

def Lean.Elab.Command.hasNoErrorMessages : Lean.Elab.Command.CommandElabM Bool

Equations

• Lean.Elab.Command.hasNoErrorMessages = do let __do_lift ← get pure !__do_lift.messages.hasErrors

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.

def Lean.Elab.Command.elabCheckFailure : Lean.Elab.Command.CommandElab

Equations

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

unsafe def Lean.Elab.Command.elabEvalCoreUnsafe (bang : Bool) (tk : Lean.Syntax) (term : Lean.Syntax) : Lean.Elab.Command.CommandElabM Unit

@[implemented_by Lean.Elab.Command.elabEvalCoreUnsafe]

opaque Lean.Elab.Command.elabEvalCore (bang : Bool) (tk : Lean.Syntax) (term : Lean.Syntax) : Lean.Elab.Command.CommandElabM Unit

def Lean.Elab.Command.elabEval : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabEvalBang : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabRunCmd : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabRunElab : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabRunMeta : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabSynth : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabSetOption : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.expandInCmd : Lean.Macro

Equations

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

def Lean.Elab.Command.elabAddDeclDoc : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabInclude : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabOmit : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabExit : Lean.Elab.Command.CommandElab

Equations

• Lean.Elab.Command.elabExit x = Lean.logWarning ((Lean.MessageData.ofFormat ∘ Lean.format) "using 'exit' to interrupt Lean")

def Lean.Elab.Command.elabImport : Lean.Elab.Command.CommandElab

Equations

• Lean.Elab.Command.elabImport x = Lean.throwError (Lean.toMessageData "invalid 'import' command, it must be used in the beginning of the file")

def Lean.Elab.Command.elabEoi : Lean.Elab.Command.CommandElab

Equations

• Lean.Elab.Command.elabEoi x = pure PUnit.unit