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 : Lean.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.

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.elabVersion : 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

def Lean.Elab.Command.elabWhere : Lean.Elab.Command.CommandElab

Equations

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

def Lean.Elab.Command.elabWhere.describeOpenDecls (ds : List Lean.OpenDecl) : Lean.Elab.Command.CommandElabM (Option Lean.MessageData)

'Delaborate' open declarations. Current limitations:

• does not check whether or not successive namespaces need _root_
• does not combine commands with renaming clauses into a single command

Equations

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

def Lean.Elab.Command.elabWhere.describeOptions (opts : Lean.Options) : Lean.Elab.Command.CommandElabM (Option Lean.MessageData)

Equations

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