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.elabEndLocalScope : CommandElab

Equations

• Lean.Elab.Command.elabEndLocalScope stx = Lean.setDelimitsLocal stx[1].toNat

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.elabDocsToVerso : CommandElab

Equations

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

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.elabReduceConfig (cfg : Syntax) (init : Meta.Command.ReduceConfig := { }) (logExceptions : Bool := true) : CommandElabM Meta.Command.ReduceConfig

Equations

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

def Lean.Elab.Command.elabReduce : CommandElab

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.elabUnlockLimits : 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 ()

def Lean.Elab.Command.elabWhere : CommandElab

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.

def Lean.Elab.Command.elabDumpAsyncEnvState : CommandElab

Equations

• Lean.Elab.Command.elabDumpAsyncEnvState x✝ = do let env ← Lean.getEnv let __do_lift ← liftM env.dbgFormatAsyncState liftM (IO.eprintln __do_lift)

def Lean.Elab.Command.elabDeprecatedModule : CommandElab

Elaborate deprecated_module, marking the current module as deprecated.

Equations

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

def Lean.Elab.Command.elabShowDeprecatedModules : CommandElab

Elaborate #show_deprecated_modules, displaying all deprecated modules.

Equations

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

def Lean.Elab.Command.elabDeprecatedSyntax : CommandElab

Equations

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