def Lean.Elab.Command.elabModuleDoc : CommandElab

Equations

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

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

Equations

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

def Lean.Elab.Command.elabNamespace : CommandElab

Equations

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

def Lean.Elab.Command.elabSection : CommandElab

Equations

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

def Lean.Elab.Command.elabEnd : CommandElab

Equations

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

def Lean.Elab.Command.elabChoice : CommandElab

Equations

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

def Lean.Elab.Command.elabUniverse : CommandElab

Equations

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

def Lean.Elab.Command.elabInitQuot : CommandElab

Equations

• Lean.Elab.Command.elabInitQuot x✝ = Lean.Elab.Command.liftCoreM (Lean.addDecl Lean.Declaration.quotDecl)

def Lean.Elab.Command.elabExport : CommandElab

Equations

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

def Lean.Elab.Command.elabOpen : CommandElab

Equations

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

def Lean.Elab.Command.elabVariable : CommandElab

Equations

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

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

Equations

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

def Lean.Elab.Command.elabCheck : CommandElab

Equations

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

def Lean.Elab.Command.elabReduce : CommandElab

Equations

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

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

Equations

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

def Lean.Elab.Command.hasNoErrorMessages : CommandElabM Bool

Equations

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

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

Equations

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

def Lean.Elab.Command.elabCheckFailure : CommandElab

Equations

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

def Lean.Elab.Command.elabSynth : CommandElab

Equations

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

def Lean.Elab.Command.elabSetOption : CommandElab

Equations

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

def Lean.Elab.Command.expandInCmd : Macro

Equations

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

def Lean.Elab.Command.elabAddDeclDoc : CommandElab

Equations

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

def Lean.Elab.Command.elabInclude : CommandElab

Equations

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

def Lean.Elab.Command.elabOmit : CommandElab

Equations

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

def Lean.Elab.Command.elabVersion : CommandElab

Equations

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

def Lean.Elab.Command.elabExit : CommandElab

Equations

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

def Lean.Elab.Command.elabImport : 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 : CommandElab

Equations

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

def Lean.Elab.Command.elabWhere : CommandElab

Equations

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

def Lean.Elab.Command.elabWhere.describeOpenDecls (ds : List OpenDecl) : CommandElabM (Option 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 : Options) : CommandElabM (Option MessageData)

Equations

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

def Lean.Elab.Command.elabWithExporting : CommandElab

Equations

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