Documentation

Lean.Elab.Command

structure Lean.Elab.Command.Scope:

Type

header : String
opts : Lean.Options
currNamespace : Lean.Name
openDecls : List Lean.OpenDecl
levelNames : List Lean.Name
section variables
varDecls : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder)
Globally unique internal identifiers for the varDecls
varUIds : Array Lean.Name
noncomputable sections automatically add the noncomputable modifier to any declaration we cannot generate code for.
isNoncomputable : Bool

instance Lean.Elab.Command.instInhabitedScope:

Inhabited Lean.Elab.Command.Scope

Equations

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

structure Lean.Elab.Command.State:

Type

env : Lean.Environment
messages : Lean.MessageLog
scopes : List Lean.Elab.Command.Scope
nextMacroScope : Nat
maxRecDepth : Nat
nextInstIdx : Nat
ngen : Lean.NameGenerator
infoState : Lean.Elab.InfoState
traceState : Lean.TraceState

instance Lean.Elab.Command.instInhabitedState:

Inhabited Lean.Elab.Command.State

Equations

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

structure Lean.Elab.Command.Context:

Type

fileName : String
fileMap : Lean.FileMap
currRecDepth : Nat
cmdPos : String.Pos
macroStack : Lean.Elab.MacroStack
currMacroScope : Lean.MacroScope
ref : Lean.Syntax
tacticCache? : Option (IO.Ref Lean.Elab.Tactic.Cache)

@[inline]

abbrev Lean.Elab.Command.CommandElabCoreM (ε : Type) (α : Type) :

Type

Equations

Lean.Elab.Command.CommandElabCoreM ε = ReaderT Lean.Elab.Command.Context (StateRefT' IO.RealWorld Lean.Elab.Command.State (EIO ε))

@[inline]

abbrev Lean.Elab.Command.CommandElabM (α : Type) :

Type

Equations

Lean.Elab.Command.CommandElabM = Lean.Elab.Command.CommandElabCoreM Lean.Exception

@[inline]

abbrev Lean.Elab.Command.CommandElab:

Type

Equations

Lean.Elab.Command.CommandElab = (Lean.Syntax → Lean.Elab.Command.CommandElabM Unit)

@[inline]

abbrev Lean.Elab.Command.Linter:

Type

Equations

Lean.Linter = (Lean.Syntax → Lean.Elab.Command.CommandElabM Unit)

instance Lean.Elab.Command.instMonadCommandElabM:

Monad Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instMonadCommandElabM = let i := inferInstanceAs (Monad Lean.Elab.Command.CommandElabM); Monad.mk

def Lean.Elab.Command.mkState (env : Lean.Environment) (messages : optParam Lean.MessageLog { msgs := { root := Std.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Std.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Std.PersistentArray.branching), size := 0, shift := Std.PersistentArray.initShift, tailOff := 0 } }) (opts : optParam Lean.Options { entries := [] }) :

Lean.Elab.Command.State

Equations

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

opaque Lean.Elab.Command.lintersRef:

IO.Ref (Array Lean.Linter)

def Lean.Elab.Command.addLinter (l : Lean.Linter) :

Equations

Lean.addLinter l = do let ls ← ST.Ref.get Lean.Elab.Command.lintersRef ST.Ref.set Lean.Elab.Command.lintersRef (Array.push ls l)

instance Lean.Elab.Command.instMonadInfoTreeCommandElabM:

Lean.Elab.MonadInfoTree Lean.Elab.Command.CommandElabM

Equations

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

instance Lean.Elab.Command.instMonadEnvCommandElabM:

Lean.MonadEnv Lean.Elab.Command.CommandElabM

Equations

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

instance Lean.Elab.Command.instMonadOptionsCommandElabM:

Lean.MonadOptions Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instMonadOptionsCommandElabM = { getOptions := do let a ← get pure (List.head! a.scopes).opts }

def Lean.Elab.Command.getRef:

Lean.Elab.Command.CommandElabM Lean.Syntax

Equations

Lean.Elab.Command.getRef = do let a ← read pure a.ref

instance Lean.Elab.Command.instAddMessageContextCommandElabM:

Lean.AddMessageContext Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instAddMessageContextCommandElabM = { addMessageContext := Lean.addMessageContextPartial }

instance Lean.Elab.Command.instMonadRefCommandElabM:

Lean.MonadRef Lean.Elab.Command.CommandElabM

Equations

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

instance Lean.Elab.Command.instMonadTraceCommandElabM:

Lean.MonadTrace Lean.Elab.Command.CommandElabM

Equations

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

instance Lean.Elab.Command.instAddErrorMessageContextCommandElabM:

Lean.AddErrorMessageContext Lean.Elab.Command.CommandElabM

Equations

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

def Lean.Elab.Command.mkMessageAux (ctx : Lean.Elab.Command.Context) (ref : Lean.Syntax) (msgData : Lean.MessageData) (severity : Lean.MessageSeverity) :

Equations

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

def Lean.Elab.Command.liftCoreM {α : Type} (x : Lean.CoreM α) :

Lean.Elab.Command.CommandElabM α

Equations

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

@[inline]

def Lean.Elab.Command.liftEIO {α : Type} (x : EIO Lean.Exception α) :

Lean.Elab.Command.CommandElabM α

Equations

Lean.Elab.Command.liftEIO x = liftM x

@[inline]

def Lean.Elab.Command.liftIO {α : Type} (x : IO α) :

Lean.Elab.Command.CommandElabM α

Equations

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

instance Lean.Elab.Command.instMonadLiftTIOCommandElabM:

MonadLiftT IO Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instMonadLiftTIOCommandElabM = { monadLift := fun {α} => Lean.Elab.Command.liftIO }

def Lean.Elab.Command.getScope:

Lean.Elab.Command.CommandElabM Lean.Elab.Command.Scope

Equations

Lean.Elab.Command.getScope = do let a ← get pure (List.head! a.scopes)

instance Lean.Elab.Command.instMonadResolveNameCommandElabM:

Lean.MonadResolveName Lean.Elab.Command.CommandElabM

Equations

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

instance Lean.Elab.Command.instMonadLogCommandElabM:

Lean.MonadLog Lean.Elab.Command.CommandElabM

Equations

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

def Lean.Elab.Command.runLinters (stx : Lean.Syntax) :

Lean.Elab.Command.CommandElabM Unit

Equations

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

def Lean.Elab.Command.getCurrMacroScope:

Lean.Elab.Command.CommandElabM Nat

Equations

Lean.Elab.Command.getCurrMacroScope = do let a ← read pure a.currMacroScope

def Lean.Elab.Command.getMainModule:

Lean.Elab.Command.CommandElabM Lean.Name

Equations

Lean.Elab.Command.getMainModule = do let a ← Lean.getEnv pure (Lean.Environment.mainModule a)

def Lean.Elab.Command.withFreshMacroScope {α : Type} (x : Lean.Elab.Command.CommandElabM α) :

Lean.Elab.Command.CommandElabM α

Equations

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

instance Lean.Elab.Command.instMonadQuotationCommandElabM:

Lean.MonadQuotation Lean.Elab.Command.CommandElabM

Equations

Lean.Elab.Command.instMonadQuotationCommandElabM = Lean.MonadQuotation.mk Lean.Elab.Command.getCurrMacroScope Lean.Elab.Command.getMainModule fun {α} => Lean.Elab.Command.withFreshMacroScope

unsafe def Lean.Elab.Command.mkCommandElabAttributeUnsafe:

IO (Lean.KeyedDeclsAttribute Lean.Elab.Command.CommandElab)

Equations

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

@[implementedBy Lean.Elab.Command.mkCommandElabAttributeUnsafe]

opaque Lean.Elab.Command.mkCommandElabAttribute:

IO (Lean.KeyedDeclsAttribute Lean.Elab.Command.CommandElab)

opaque Lean.Elab.Command.commandElabAttribute:

Lean.KeyedDeclsAttribute Lean.Elab.Command.CommandElab

def Lean.Elab.Command.withMacroExpansion {α : Type} (beforeStx : Lean.Syntax) (afterStx : Lean.Syntax) (x : Lean.Elab.Command.CommandElabM α) :

Lean.Elab.Command.CommandElabM α

Equations

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

instance Lean.Elab.Command.instMonadMacroAdapterCommandElabM:

Lean.Elab.MonadMacroAdapter Lean.Elab.Command.CommandElabM

Equations

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

instance Lean.Elab.Command.instMonadRecDepthCommandElabM:

Lean.MonadRecDepth Lean.Elab.Command.CommandElabM

Equations

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

opaque Lean.Elab.Command.showPartialSyntaxErrors:

Lean.Option Bool

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

Lean.Elab.Command.CommandElabM Unit

Equations

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

partial def Lean.Elab.Command.elabCommand (stx : Lean.Syntax) :

Lean.Elab.Command.CommandElabM Unit

def Lean.Elab.Command.elabCommandTopLevel (stx : Lean.Syntax) :

Lean.Elab.Command.CommandElabM Unit

elabCommand wrapper that should be used for the initial invocation, not for recursive calls after macro expansion etc.

Equations

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

def Lean.Elab.Command.adaptExpander (exp : Lean.Syntax → Lean.Elab.Command.CommandElabM Lean.Syntax) :

Lean.Elab.Command.CommandElab

Adapt a syntax transformation to a regular, command-producing elaborator.

Equations

Lean.Elab.Command.adaptExpander exp stx = do let stx' ← exp stx Lean.Elab.Command.withMacroExpansion stx stx' (Lean.Elab.Command.elabCommand stx')

instance Lean.Elab.Command.instInhabitedCommandElabM {α : Type} :

Inhabited (Lean.Elab.Command.CommandElabM α)

Equations

Lean.Elab.Command.instInhabitedCommandElabM = { default := throw default }

def Lean.Elab.Command.getBracketedBinderIds:

Lean.Syntax → Array Lean.Name

Equations

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

def Lean.Elab.Command.liftTermElabM {α : Type} (declName? : Option Lean.Name) (x : Lean.Elab.TermElabM α) :

Lean.Elab.Command.CommandElabM α

Equations

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

@[inline]

def Lean.Elab.Command.runTermElabM {α : Type} (declName? : Option Lean.Name) (elabFn : Array Lean.Expr → Lean.Elab.TermElabM α) :

Lean.Elab.Command.CommandElabM α

Equations

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

@[inline]

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

Lean.Elab.Command.CommandElabCoreM Empty Unit

Equations

Lean.Elab.Command.catchExceptions x ctx ref = EIO.catchExceptions (Lean.Elab.Command.withLogging x ctx ref) fun x => pure ()

def Lean.Elab.Command.getScopes:

Lean.Elab.Command.CommandElabM (List Lean.Elab.Command.Scope)

Equations

Lean.Elab.Command.getScopes = do let a ← get pure a.scopes

def Lean.Elab.Command.modifyScope (f : Lean.Elab.Command.Scope → Lean.Elab.Command.Scope) :

Lean.Elab.Command.CommandElabM Unit

Equations

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

def Lean.Elab.Command.withScope {α : Type} (f : Lean.Elab.Command.Scope → Lean.Elab.Command.Scope) (x : 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.getLevelNames:

Lean.Elab.Command.CommandElabM (List Lean.Name)

Equations

Lean.Elab.Command.getLevelNames = do let a ← Lean.Elab.Command.getScope pure a.levelNames

def Lean.Elab.Command.addUnivLevel (idStx : Lean.Syntax) :

Lean.Elab.Command.CommandElabM Unit

Equations

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

def Lean.Elab.Command.expandDeclId (declId : Lean.Syntax) (modifiers : Lean.Elab.Modifiers) :

Lean.Elab.Command.CommandElabM Lean.Elab.ExpandDeclIdResult

Equations

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