structure Lean.Elab.Term.SavedContext : Type

Saved context for postponed terms and tactics to be executed.

• declName? : Option Name
• options : Options
• openDecls : List OpenDecl
• macroStack : MacroStack
• errToSorry : Bool
• levelNames : List Name

inductive Lean.Elab.Term.TacticMVarKind : Type

The kind of a tactic metavariable, used for additional error reporting.

• term : TacticMVarKind

  Standard tactic metavariable, arising from by ... syntax.

• autoParam (argName : Name) : TacticMVarKind

  Tactic metavariable arising from an autoparam for a function application.

• fieldAutoParam (fieldName structName : Name) : TacticMVarKind

  Tactic metavariable arising from an autoparam for a structure field.

inductive Lean.Elab.Term.SyntheticMVarKind : Type

We use synthetic metavariables as placeholders for pending elaboration steps.

• typeClass (extraErrorMsg? : Option MessageData) : SyntheticMVarKind

  Use typeclass resolution to synthesize value for metavariable. If extraErrorMsg? is some msg, msg contains additional information to include in error messages regarding type class synthesis failure.

• coe (header? : Option String) (expectedType e : Expr) (f? : Option Expr) (mkErrorMsg? : Option (MVarId → Expr → Expr → MetaM MessageData)) : SyntheticMVarKind

  Use coercion to synthesize value for the metavariable. If synthesis fails, then throws an error.

  • If mkErrorMsg? is provided, then the error mkErrorMsg expectedType e is thrown. The mkErrorMsg function is allowed to throw an error itself.
  • Otherwise, throws a default type mismatch error message. If header? is not provided, the default header is "type mismatch". If f? is provided, then throws an application type mismatch error.
• tactic (tacticCode : Syntax) (ctx : SavedContext) (kind : TacticMVarKind) (delayOnMVars : Bool := false) : SyntheticMVarKind

  Use tactic to synthesize value for metavariable.

  If delayOnMVars is true, the tactic will not be executed until the goal is free of unassigned expr metavariables.

• postponed (ctx : SavedContext) : SyntheticMVarKind

  Metavariable represents a hole whose elaboration has been postponed.

instance Lean.Elab.Term.instInhabitedSyntheticMVarKind : Inhabited SyntheticMVarKind

Equations

• Lean.Elab.Term.instInhabitedSyntheticMVarKind = { default := Lean.Elab.Term.instInhabitedSyntheticMVarKind.default }

def Lean.Elab.Term.instInhabitedSyntheticMVarKind.default : SyntheticMVarKind

Equations

• Lean.Elab.Term.instInhabitedSyntheticMVarKind.default = Lean.Elab.Term.SyntheticMVarKind.typeClass default

def Lean.Elab.Term.extraMsgToMsg (extraErrorMsg? : Option MessageData) : MessageData

Convert an "extra" optional error message into a message "\n{msg}" (if some msg) and MessageData.nil (if none)

Equations

• Lean.Elab.Term.extraMsgToMsg (some msg) = Lean.toMessageData "\n" ++ Lean.toMessageData msg
• Lean.Elab.Term.extraMsgToMsg extraErrorMsg? = Lean.MessageData.nil

instance Lean.Elab.Term.instToStringSyntheticMVarKind : ToString SyntheticMVarKind

Equations

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

structure Lean.Elab.Term.SyntheticMVarDecl : Type

• stx : Syntax
• kind : SyntheticMVarKind

instance Lean.Elab.Term.instInhabitedSyntheticMVarDecl : Inhabited SyntheticMVarDecl

Equations

• Lean.Elab.Term.instInhabitedSyntheticMVarDecl = { default := Lean.Elab.Term.instInhabitedSyntheticMVarDecl.default }

def Lean.Elab.Term.instInhabitedSyntheticMVarDecl.default : SyntheticMVarDecl

Equations

• Lean.Elab.Term.instInhabitedSyntheticMVarDecl.default = { stx := default, kind := default }

inductive Lean.Elab.Term.MVarErrorKind : Type

We can optionally associate an error context with a metavariable (see MVarErrorInfo). We have three different kinds of error context.

• implicitArg (lctx : LocalContext) (ctx : Expr) : MVarErrorKind

  Metavariable for implicit arguments. ctx is the parent application, lctx is a local context where it is valid (necessary for eta feature for named arguments).

• hole : MVarErrorKind

  Metavariable for explicit holes provided by the user (e.g., _ and ?m)

• custom (msgData : MessageData) : MVarErrorKind

  "Custom", msgData stores the additional error messages.

instance Lean.Elab.Term.instInhabitedMVarErrorKind : Inhabited MVarErrorKind

Equations

• Lean.Elab.Term.instInhabitedMVarErrorKind = { default := Lean.Elab.Term.instInhabitedMVarErrorKind.default }

def Lean.Elab.Term.instInhabitedMVarErrorKind.default : MVarErrorKind

Equations

• Lean.Elab.Term.instInhabitedMVarErrorKind.default = Lean.Elab.Term.MVarErrorKind.implicitArg default default

instance Lean.Elab.Term.instToStringMVarErrorKind : ToString MVarErrorKind

Equations

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

structure Lean.Elab.Term.MVarErrorInfo : Type

We can optionally associate an error context with metavariables.

• mvarId : MVarId
• ref : Syntax
• kind : MVarErrorKind

instance Lean.Elab.Term.instInhabitedMVarErrorInfo : Inhabited MVarErrorInfo

Equations

• Lean.Elab.Term.instInhabitedMVarErrorInfo = { default := Lean.Elab.Term.instInhabitedMVarErrorInfo.default }

def Lean.Elab.Term.instInhabitedMVarErrorInfo.default : MVarErrorInfo

Equations

• Lean.Elab.Term.instInhabitedMVarErrorInfo.default = { mvarId := default, ref := default, kind := default }

structure Lean.Elab.Term.LevelMVarErrorInfo : Type

When reporting unexpected universe level metavariables, it is useful to localize the errors to particular terms, especially at let bindings and function binders, where universe polymorphism is not permitted.

• lctx : LocalContext
• expr : Expr
• ref : Syntax
• msgData? : Option MessageData

instance Lean.Elab.Term.instInhabitedLevelMVarErrorInfo : Inhabited LevelMVarErrorInfo

Equations

• Lean.Elab.Term.instInhabitedLevelMVarErrorInfo = { default := Lean.Elab.Term.instInhabitedLevelMVarErrorInfo.default }

def Lean.Elab.Term.instInhabitedLevelMVarErrorInfo.default : LevelMVarErrorInfo

Equations

• Lean.Elab.Term.instInhabitedLevelMVarErrorInfo.default = { lctx := default, expr := default, ref := default, msgData? := default }

structure Lean.Elab.Term.LetRecToLift : Type

Nested let rec expressions are eagerly lifted by the elaborator. We store the information necessary for performing the lifting here.

• ref : Syntax
• fvarId : FVarId
• attrs : Array Attribute
• shortDeclName : Name
• declName : Name
• parentName? : Option Name
• lctx : LocalContext
• localInstances : LocalInstances
• type : Expr
• val : Expr
• mvarId : MVarId
• termination : TerminationHints

def Lean.Elab.Term.instInhabitedLetRecToLift.default : LetRecToLift

Equations

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

instance Lean.Elab.Term.instInhabitedLetRecToLift : Inhabited LetRecToLift

Equations

• Lean.Elab.Term.instInhabitedLetRecToLift = { default := Lean.Elab.Term.instInhabitedLetRecToLift.default }

structure Lean.Elab.Term.State : Type

State of the TermElabM monad.

• levelNames : List Name
• syntheticMVars : MVarIdMap SyntheticMVarDecl
• pendingMVars : List MVarId
• mvarErrorInfos : List MVarErrorInfo

  List of errors associated to a metavariable that are shown to the user if the metavariable could not be fully instantiated

• levelMVarErrorInfos : List LevelMVarErrorInfo

  List of data to be able to localize universe level metavariable errors to particular expressions.

• mvarArgNames : MVarIdMap Name

  mvarArgNames stores the argument names associated to metavariables. These are used in combination with mvarErrorInfos for throwing errors about metavariables that could not be fully instantiated. For example when elaborating List _, the argument name of the placeholder will be α.

  While elaborating an application, mvarArgNames is set for each metavariable argument, using the available argument name. This may happen before or after the mvarErrorInfos is set for the same metavariable.

  We used to store the argument names in mvarErrorInfos, updating the MVarErrorInfos to add the argument name when it is available, but this doesn't work if the argument name is available before the mvarErrorInfos is set for that metavariable.

• letRecsToLift : List LetRecToLift

instance Lean.Elab.Term.instInhabitedState : Inhabited State

Equations

• Lean.Elab.Term.instInhabitedState = { default := Lean.Elab.Term.instInhabitedState.default }

def Lean.Elab.Term.instInhabitedState.default : State

Equations

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

structure Lean.Elab.Term.SavedState : Type

Backtrackable state for the TermElabM monad.

• meta : Meta.SavedState
• elab : State

instance Lean.Elab.Term.instNonemptySavedState : Nonempty SavedState

structure Lean.Elab.Tactic.State : Type

State of the TacticM monad.

• goals : List MVarId

def Lean.Elab.Tactic.instInhabitedState.default : State

Equations

• Lean.Elab.Tactic.instInhabitedState.default = { goals := default }

instance Lean.Elab.Tactic.instInhabitedState : Inhabited State

Equations

• Lean.Elab.Tactic.instInhabitedState = { default := Lean.Elab.Tactic.instInhabitedState.default }

structure Lean.Elab.Tactic.Snapshot : Type

Snapshots are used to implement the save tactic. This tactic caches the state of the system, and allows us to "replay" expensive proofs efficiently. This is only relevant implementing the LSP server.

• core : Core.State
• meta : Meta.State
• term : Term.State
• tactic : State
• stx : Syntax

structure Lean.Elab.Tactic.CacheKey : Type

Key for the cache used to implement the save tactic.

• mvarId : MVarId
• pos : String.Pos

def Lean.Elab.Tactic.instBEqCacheKey.beq : CacheKey → CacheKey → Bool

Equations

• Lean.Elab.Tactic.instBEqCacheKey.beq { mvarId := a, pos := a_1 } { mvarId := b, pos := b_1 } = (a == b && a_1 == b_1)
• Lean.Elab.Tactic.instBEqCacheKey.beq x✝¹ x✝ = false

instance Lean.Elab.Tactic.instBEqCacheKey : BEq CacheKey

Equations

• Lean.Elab.Tactic.instBEqCacheKey = { beq := Lean.Elab.Tactic.instBEqCacheKey.beq }

def Lean.Elab.Tactic.instHashableCacheKey.hash : CacheKey → UInt64

Equations

• Lean.Elab.Tactic.instHashableCacheKey.hash { mvarId := a, pos := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

instance Lean.Elab.Tactic.instHashableCacheKey : Hashable CacheKey

Equations

• Lean.Elab.Tactic.instHashableCacheKey = { hash := Lean.Elab.Tactic.instHashableCacheKey.hash }

def Lean.Elab.Tactic.instInhabitedCacheKey.default : CacheKey

Equations

• Lean.Elab.Tactic.instInhabitedCacheKey.default = { mvarId := default, pos := default }

instance Lean.Elab.Tactic.instInhabitedCacheKey : Inhabited CacheKey

Equations

• Lean.Elab.Tactic.instInhabitedCacheKey = { default := Lean.Elab.Tactic.instInhabitedCacheKey.default }

structure Lean.Elab.Tactic.Cache : Type

Cache for the save tactic.

• pre : PHashMap CacheKey Snapshot
• post : PHashMap CacheKey Snapshot

instance Lean.Elab.Tactic.instInhabitedCache : Inhabited Cache

Equations

• Lean.Elab.Tactic.instInhabitedCache = { default := Lean.Elab.Tactic.instInhabitedCache.default }

def Lean.Elab.Tactic.instInhabitedCache.default : Cache

Equations

• Lean.Elab.Tactic.instInhabitedCache.default = { pre := default, post := default }

structure Lean.Elab.Tactic.SavedState : Type

• term : Term.SavedState
• tactic : State

structure Lean.Elab.Tactic.TacticFinishedSnapshotextends Lean.Language.Snapshot : Type

Snapshot after finishing execution of a tactic.

• desc : String
• diagnostics : Diagnostics
• infoTree? : Option Elab.InfoTree
• traces : TraceState
• isFatal : Bool
• state? : Option SavedState

  State saved for reuse, if no fatal exception occurred.

• moreSnaps : Array (Language.SnapshotTask Language.SnapshotTree)

  Untyped snapshots from logSnapshotTask, saved at this level for cancellation.

instance Lean.Elab.Tactic.instInhabitedTacticFinishedSnapshot : Inhabited TacticFinishedSnapshot

Equations

• Lean.Elab.Tactic.instInhabitedTacticFinishedSnapshot = { default := Lean.Elab.Tactic.instInhabitedTacticFinishedSnapshot.default }

def Lean.Elab.Tactic.instInhabitedTacticFinishedSnapshot.default : TacticFinishedSnapshot

Equations

• Lean.Elab.Tactic.instInhabitedTacticFinishedSnapshot.default = { toSnapshot := default, state? := default, moreSnaps := default }

instance Lean.Elab.Tactic.instToSnapshotTreeTacticFinishedSnapshot : Language.ToSnapshotTree TacticFinishedSnapshot

Equations

• Lean.Elab.Tactic.instToSnapshotTreeTacticFinishedSnapshot = { toSnapshotTree := fun (s : Lean.Elab.Tactic.TacticFinishedSnapshot) => { element := s.toSnapshot, children := s.moreSnaps } }

structure Lean.Elab.Tactic.TacticParsedSnapshotextends Lean.Language.Snapshot : Type

Snapshot just before execution of a tactic.

• desc : String
• diagnostics : Diagnostics
• infoTree? : Option Elab.InfoTree
• traces : TraceState
• isFatal : Bool
• stx : Syntax

  Syntax tree of the tactic, stored and compared for incremental reuse.

• inner? : Option (Language.SnapshotTask TacticParsedSnapshot)

  Task for nested incrementality, if enabled for tactic.

• finished : Language.SnapshotTask TacticFinishedSnapshot

  Task for state after tactic execution.

• next : Array (Language.SnapshotTask TacticParsedSnapshot)

  Tasks for subsequent, potentially parallel, tactic steps.

def Lean.Elab.Tactic.instInhabitedTacticParsedSnapshot.default : TacticParsedSnapshot

Equations

• Lean.Elab.Tactic.instInhabitedTacticParsedSnapshot.default = { toSnapshot := default, stx := default, inner? := default, finished := default, next := default }

instance Lean.Elab.Tactic.instInhabitedTacticParsedSnapshot : Inhabited TacticParsedSnapshot

Equations

• Lean.Elab.Tactic.instInhabitedTacticParsedSnapshot = { default := Lean.Elab.Tactic.instInhabitedTacticParsedSnapshot.default }

instance Lean.Elab.Tactic.instToSnapshotTreeTacticParsedSnapshot : Language.ToSnapshotTree TacticParsedSnapshot

Equations

• Lean.Elab.Tactic.instToSnapshotTreeTacticParsedSnapshot = { toSnapshotTree := Lean.Elab.Tactic.instToSnapshotTreeTacticParsedSnapshot.go }

partial def Lean.Elab.Tactic.instToSnapshotTreeTacticParsedSnapshot.go (s : TacticParsedSnapshot) : Language.SnapshotTree

structure Lean.Elab.Term.Context : Type

• declName? : Option Name
• macroStack : MacroStack
• mayPostpone : Bool

  When mayPostpone == true, an elaboration function may interrupt its execution by throwing Exception.postpone. The function elabTerm catches this exception and creates fresh synthetic metavariable ?m, stores ?m in the list of pending synthetic metavariables, and returns ?m.

• errToSorry : Bool

  When errToSorry is set to true, the method elabTerm catches exceptions and converts them into synthetic sorrys. The implementation of choice nodes and overloaded symbols rely on the fact that when errToSorry is set to false for an elaboration function F, then errToSorry remains false for all elaboration functions invoked by F. That is, it is safe to transition errToSorry from true to false, but we must not set errToSorry to true when it is currently set to false.

• autoBoundImplicit : Bool

  When autoBoundImplicit is set to true, instead of producing an "unknown identifier" error for unbound variables, we generate an internal exception. This exception is caught at withAutoBoundImplicit which adds an implicit declaration for the unbound variable and tries again.

• autoBoundImplicits : PArray Expr
• autoBoundImplicitForbidden : Name → Bool

  A name n is only eligible to be an auto implicit name if autoBoundImplicitForbidden n = false. We use this predicate to disallow f to be considered an auto implicit name in a definition such as

  def f : f → Bool := fun _ => true
  

• sectionVars : NameMap Name

  Map from user name to internal unique name

• sectionFVars : NameMap Expr

  Map from internal name to fvar

• implicitLambda : Bool

  Enable/disable implicit lambdas feature.

• heedElabAsElim : Bool

  Heed elab_as_elim attribute.

• isNoncomputableSection : Bool

  Noncomputable sections automatically add the noncomputable modifier to any declaration we cannot generate code for.

• ignoreTCFailures : Bool

  When true we skip TC failures. We use this option when processing patterns.

• inPattern : Bool

  true when elaborating patterns. It affects how we elaborate named holes.

• tacSnap? : Option (Language.SnapshotBundle Tactic.TacticParsedSnapshot)

  Snapshot for incremental processing of current tactic, if any.

  Invariant: if the bundle's old? is set, then the state up to the start of the tactic is unchanged, i.e. reuse is possible.

• saveRecAppSyntax : Bool

  If true, we store in the Expr the Syntax for recursive applications (i.e., applications of free variables tagged with isAuxDecl). We store the Syntax using mkRecAppWithSyntax. We use the Syntax object to produce better error messages at Structural.lean and WF.lean.

• holesAsSyntheticOpaque : Bool

  If holesAsSyntheticOpaque is true, then we mark metavariables associated with _s as syntheticOpaque if they do not occur in patterns. This option is useful when elaborating terms in tactics such as refine' where we want holes there to become new goals. See issue #1681, we have `refine' (fun x => _)

• checkDeprecated : Bool

  If checkDeprecated := true, then Linter.checkDeprecated when creating constants.

@[reducible, inline]

abbrev Lean.Elab.Term.TermElabM (α : Type) : Type

Equations

• Lean.Elab.TermElabM = ReaderT Lean.Elab.Term.Context (StateRefT' IO.RealWorld Lean.Elab.Term.State Lean.MetaM)

@[reducible, inline]

abbrev Lean.Elab.Term.TermElab : Type

Equations

• Lean.Elab.Term.TermElab = (Lean.Syntax → Option Lean.Expr → Lean.Elab.TermElabM Lean.Expr)

@[always_inline]

instance Lean.Elab.Term.instMonadTermElabM : Monad TermElabM

Equations

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

instance Lean.Elab.Term.instInhabitedTermElabM {α : Type} : Inhabited (TermElabM α)

Equations

• Lean.Elab.Term.instInhabitedTermElabM = { default := throw default }

def Lean.Elab.Term.saveState : TermElabM SavedState

Equations

• Lean.Elab.Term.saveState = do let __do_lift ← liftM Lean.Meta.saveState let __do_lift_1 ← get pure { «meta» := __do_lift, «elab» := __do_lift_1 }

def Lean.Elab.Term.SavedState.restore (s : SavedState) (restoreInfo : Bool := false) : TermElabM Unit

Equations

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

@[specialize #[]]

def Lean.Elab.Term.withRestoreOrSaveFull {α : Type} (reusableResult? : Option (α × SavedState)) (tacSnap? : Option (Language.SnapshotBundle Tactic.TacticParsedSnapshot)) (act : TermElabM α) : TermElabM (α × SavedState)

Like Meta.withRestoreOrSaveFull for TermElabM, but also takes a tacSnap? that

• when running act, is set as Context.tacSnap?
• otherwise (i.e. on restore) is used to update the new snapshot promise to the old task's value. This extra restore step is necessary because while reusableResult? can be used to replay any effects on State, Context.tacSnap? is not part of it but changed via an IO side effect, so it needs to be replayed separately.

We use an explicit parameter instead of accessing Context.tacSnap? directly because this prevents withRestoreOrSaveFull and withReader from being used in the wrong order.

Equations

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

instance Lean.Elab.Term.instMonadBacktrackSavedStateTermElabM : MonadBacktrack SavedState TermElabM

Equations

• Lean.Elab.Term.instMonadBacktrackSavedStateTermElabM = { saveState := Lean.Elab.Term.saveState, restoreState := fun (b : Lean.Elab.Term.SavedState) => b.restore }

def Lean.Elab.Term.withReuseContext {m : Type → Type u_1} {α : Type} [Monad m] [MonadWithReaderOf Core.Context m] (stx : Syntax) (act : m α) : m α

Incremental elaboration helper. Avoids leakage of data from outside syntax via the monadic context when running act on stx by

• setting stx as the ref and
• deactivating suppressElabErrors if stx is missing-free, which also helps with not hiding useful errors in this part of the input. Note that if stx has missing, this should always be true for the outer syntax as well, so taking the old value of suppressElabErrors into account should not introduce data leakage.

This combinator should always be used when narrowing reuse to a syntax subtree, usually (in the case of tactics, to be generalized) via withNarrowed(Arg)TacticReuse.

Equations

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

def Lean.Elab.Term.withNarrowedTacticReuse {m : Type → Type} {α : Type} [Monad m] [MonadReaderOf Context m] [MonadLiftT BaseIO m] [MonadWithReaderOf Core.Context m] [MonadWithReaderOf Context m] [MonadOptions m] (split : Syntax → Syntax × Syntax) (act : Syntax → m α) (stx : Syntax) : m α

Manages reuse information for nested tactics by splitting given syntax into an outer and inner part. act is then run on the inner part but with reuse information adjusted as following:

• If the old (from tacSnap?'s SyntaxGuarded.stx) and new (from stx) outer syntax are not identical according to Syntax.eqWithInfo, reuse is disabled.
• Otherwise, the old syntax as stored in tacSnap? is updated to the old inner syntax.
• In any case, withReuseContext is used on the new inner syntax to further prepare the monadic context.

For any tactic that participates in reuse, withNarrowedTacticReuse should be applied to the tactic's syntax and act should be used to do recursive tactic evaluation of nested parts. Also, after this function, getAndEmptySnapshotTasks should be called and the result stored in a snapshot so that the tasks don't end up in a snapshot further up and are cancelled together with it; see note [Incremental Cancellation].

Equations

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

def Lean.Elab.Term.withNarrowedArgTacticReuse {m : Type → Type} {α : Type} [Monad m] [MonadReaderOf Context m] [MonadLiftT BaseIO m] [MonadWithReaderOf Core.Context m] [MonadWithReaderOf Context m] [MonadOptions m] (argIdx : Nat) (act : Syntax → m α) (stx : Syntax) : m α

A variant of withNarrowedTacticReuse that uses stx[argIdx] as the inner syntax and all stx child nodes before that as the outer syntax, i.e. reuse is disabled if there was any change before argIdx.

NOTE: child nodes after argIdx are not tested (which would almost always disable reuse as they are necessarily shifted by changes at argIdx) so it must be ensured that the result of arg does not depend on them (i.e. they should not be inspected beforehand).

Equations

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

def Lean.Elab.Term.withoutTacticIncrementality {m : Type → Type} {α : Type} [Monad m] [MonadWithReaderOf Context m] [MonadOptions m] (cond : Bool) (act : m α) : m α

Disables incremental tactic reuse and reporting for act if cond is true by setting tacSnap? to none. This should be done for tactic blocks that are run multiple times as otherwise the reported progress will jump back and forth (and partial reuse for these kinds of tact blocks is similarly questionable).

Equations

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

def Lean.Elab.Term.withoutTacticReuse {m : Type → Type} {α : Type} [Monad m] [MonadWithReaderOf Context m] [MonadOptions m] (cond : Bool) (act : m α) : m α

Disables incremental tactic reuse for act if cond is true.

Equations

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

def Lean.Elab.Term.wrapAsyncAsSnapshot {α : Type} (act : α → TermElabM Unit) (cancelTk? : Option IO.CancelToken) (desc : String := by exact decl_name%.toString) : TermElabM (α → BaseIO Language.SnapshotTree)

Wraps the given action for use in BaseIO.asTask etc., discarding its final state except for logSnapshotTask tasks, which are reported as part of the returned tree. The given cancellation token, if any, should be stored in a SnapshotTask for the server to trigger it when the result is no longer needed.

Equations

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

@[reducible, inline]

abbrev Lean.Elab.Term.TermElabResult (α : Type) : Type

Equations

• Lean.Elab.Term.TermElabResult α = EStateM.Result Lean.Exception Lean.Elab.Term.SavedState α

def Lean.Elab.Term.observing {α : Type} (x : TermElabM α) : TermElabM (TermElabResult α)

Execute x, save resulting expression and new state. We remove any Info created by x. The info nodes are committed when we execute applyResult. We use observing to implement overloaded notation and decls. We want to save Info nodes for the chosen alternative.

Equations

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

def Lean.Elab.Term.applyResult {α : Type} (result : TermElabResult α) : TermElabM α

Apply the result/exception and state captured with observing. We use this method to implement overloaded notation and symbols.

Equations

• Lean.Elab.Term.applyResult (EStateM.Result.ok a r) = do r.restore true pure a
• Lean.Elab.Term.applyResult (EStateM.Result.error ex r) = do r.restore true throw ex

def Lean.Elab.Term.commitIfDidNotPostpone {α : Type} (x : TermElabM α) : TermElabM α

Execute x, but keep state modifications only if x did not postpone. This method is useful to implement elaboration functions that cannot decide whether they need to postpone or not without updating the state.

Equations

• Lean.Elab.Term.commitIfDidNotPostpone x = do let r ← Lean.Elab.Term.observing x Lean.Elab.Term.applyResult r

def Lean.Elab.Term.getLevelNames : TermElabM (List Name)

Return the universe level names explicitly provided by the user.

Equations

• Lean.Elab.Term.getLevelNames = do let __do_lift ← get pure __do_lift.levelNames

def Lean.Elab.Term.getFVarLocalDecl! (fvar : Expr) : TermElabM LocalDecl

Given a free variable fvar, return its declaration. This function panics if fvar is not a free variable.

Equations

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

instance Lean.Elab.Term.instAddErrorMessageContextTermElabM : AddErrorMessageContext TermElabM

Equations

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

def Lean.Elab.Term.withoutSavingRecAppSyntax {α : Type} (x : TermElabM α) : TermElabM α

Execute x without storing Syntax for recursive applications. See saveRecAppSyntax field at Context.

Equations

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

unsafe def Lean.Elab.Term.mkTermElabAttributeUnsafe (ref : Name) : IO (KeyedDeclsAttribute TermElab)

Equations

• Lean.Elab.Term.mkTermElabAttributeUnsafe ref = Lean.Elab.mkElabAttribute Lean.Elab.Term.TermElab `builtin_term_elab `term_elab `Lean.Parser.Term `Lean.Elab.Term.TermElab "term" ref

@[implemented_by Lean.Elab.Term.mkTermElabAttributeUnsafe]

opaque Lean.Elab.Term.mkTermElabAttribute (ref : Name) : IO (KeyedDeclsAttribute TermElab)

opaque Lean.Elab.Term.termElabAttribute : KeyedDeclsAttribute TermElab

Registers a term elaborator for the given syntax node kind.

A term elaborator should have type Lean.Elab.Term.TermElab (which is Lean.Syntax → Option Lean.Expr → Lean.Elab.Term.TermElabM Lean.Expr), i.e. should take syntax of the given syntax node kind and an optional expected type as parameters and produce an expression.

The elab_rules and elab commands should usually be preferred over using this attribute directly.

inductive Lean.Elab.Term.LVal : Type

Auxiliary datatype for presenting a Lean lvalue modifier. We represent an unelaborated lvalue as a Syntax (or Expr) and List LVal. Example: a.foo.1 is represented as the Syntax a and the list [LVal.fieldName "foo", LVal.fieldIdx 1].

• fieldIdx (ref : Syntax) (i : Nat) : LVal
• fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (fullRef : Syntax) : LVal

  Field suffix? is for producing better error messages because x.y may be a field access or a hierarchical/composite name. ref is the syntax object representing the field. fullRef includes the LHS.

def Lean.Elab.Term.LVal.getRef : LVal → Syntax

Equations

• (Lean.Elab.Term.LVal.fieldIdx ref i).getRef = ref
• (Lean.Elab.Term.LVal.fieldName ref name suffix? fullRef).getRef = ref

def Lean.Elab.Term.LVal.isFieldName : LVal → Bool

Equations

• (Lean.Elab.Term.LVal.fieldName ref name suffix? fullRef).isFieldName = true
• x✝.isFieldName = false

instance Lean.Elab.Term.instToStringLVal : ToString LVal

Equations

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

def Lean.Elab.Term.getDeclName? : TermElabM (Option Name)

Return the name of the declaration being elaborated if available.

Equations

• Lean.Elab.Term.getDeclName? = do let __do_lift ← read pure __do_lift.declName?

def Lean.Elab.Term.getLetRecsToLift : TermElabM (List LetRecToLift)

Return the list of nested let rec declarations that need to be lifted.

Equations

• Lean.Elab.Term.getLetRecsToLift = do let __do_lift ← get pure __do_lift.letRecsToLift

def Lean.Elab.Term.getMVarDecl (mvarId : MVarId) : TermElabM MetavarDecl

Return the declaration of the given metavariable

Equations

• Lean.Elab.Term.getMVarDecl mvarId = do let __do_lift ← Lean.getMCtx pure (__do_lift.getDecl mvarId)

instance Lean.Elab.Term.instMonadParentDeclTermElabM : MonadParentDecl TermElabM

Equations

• Lean.Elab.Term.instMonadParentDeclTermElabM = { getParentDeclName? := Lean.Elab.Term.getDeclName? }

def Lean.Elab.Term.withDeclName {α : Type} (name : Name) (x : TermElabM α) : TermElabM α

Executes x in the context of the given declaration name. Ensures that the info tree is set up correctly and adjusts the declaration name generator to generate names below this name, resetting the nested counter.

Equations

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

def Lean.Elab.Term.setLevelNames (levelNames : List Name) : TermElabM Unit

Update the universe level parameter names.

Equations

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

def Lean.Elab.Term.withLevelNames {α : Type} (levelNames : List Name) (x : TermElabM α) : TermElabM α

Execute x using levelNames as the universe level parameter names. See getLevelNames.

Equations

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

def Lean.Elab.Term.withoutErrToSorryImp {α : Type} (x : TermElabM α) : TermElabM α

Equations

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

def Lean.Elab.Term.withoutErrToSorry {m : Type → Type u_1} {α : Type} [MonadFunctorT TermElabM m] : m α → m α

Execute x without converting errors (i.e., exceptions) to sorry applications. Recall that when errToSorry = true, the method elabTerm catches exceptions and converts them into sorry applications.

Equations

• Lean.Elab.Term.withoutErrToSorry = monadMap fun {β : Type} => Lean.Elab.Term.withoutErrToSorryImp

def Lean.Elab.Term.withoutHeedElabAsElimImp {α : Type} (x : TermElabM α) : TermElabM α

Equations

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

def Lean.Elab.Term.withoutHeedElabAsElim {m : Type → Type u_1} {α : Type} [MonadFunctorT TermElabM m] : m α → m α

Execute x without heeding the elab_as_elim attribute. Useful when there is no expected type (so elabAppArgs would fail), but expect that the user wants to use such constants.

Equations

• Lean.Elab.Term.withoutHeedElabAsElim = monadMap fun {β : Type} => Lean.Elab.Term.withoutHeedElabAsElimImp

def Lean.Elab.Term.withoutModifyingElabMetaStateWithInfo {α : Type} (x : TermElabM α) : TermElabM α

Execute x but discard changes performed at Term.State and Meta.State. Recall that the Environment, InfoState and messages are at Core.State. Thus, any updates to it will be preserved. This method is useful for performing computations where all metavariable must be resolved or discarded. The InfoTrees are not discarded, however, and wrapped in InfoTree.Context to store their metavariable context.

Equations

• Lean.Elab.Term.withoutModifyingElabMetaStateWithInfo x = do let s ← get let sMeta ← getThe Lean.Meta.State tryFinally (Lean.Elab.withSaveInfoContext x) do set s set sMeta

def Lean.Elab.Term.getInfoTreeWithContext? : TermElabM (Option InfoTree)

Wraps the trees returned from getInfoTrees, if any, in an InfoTree.context node based on the current monadic context and state. This is mainly used to report info trees early via Snapshot.infoTree?. The trees are not removed from the getInfoTrees state as the final info tree of the elaborated command should be complete and not depend on whether parts have been reported early.

As InfoTree.context can have only one child, this function panics if trees contains more than 1 tree. Also, PartialContextInfo.parentDeclCtx is not currently generated as that information is not available in the monadic context and only needed for the final info tree.

Equations

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

def Lean.Elab.Term.throwErrorIfErrors : TermElabM Unit

For testing TermElabM methods. The #eval command will sign the error.

Equations

• Lean.Elab.Term.throwErrorIfErrors = do let __do_lift ← Lean.MonadLog.hasErrors if __do_lift = true then Lean.throwError (Lean.toMessageData "Error(s)") else pure PUnit.unit

def Lean.Elab.Term.traceAtCmdPos (cls : Name) (msg : Unit → MessageData) : TermElabM Unit

Equations

• Lean.Elab.Term.traceAtCmdPos cls msg = Lean.withRef Lean.Syntax.missing (Lean.trace cls msg)

def Lean.Elab.Term.ppGoal (mvarId : MVarId) : TermElabM Format

Equations

• Lean.Elab.Term.ppGoal mvarId = liftM (Lean.Meta.ppGoal mvarId)

def Lean.Elab.Term.liftLevelM {α : Type} (x : Level.LevelElabM α) : TermElabM α

Equations

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

def Lean.Elab.Term.elabLevel (stx : Syntax) : TermElabM Level

Equations

• Lean.Elab.Term.elabLevel stx = Lean.Elab.Term.liftLevelM (Lean.Elab.Level.elabLevel stx)

def Lean.Elab.Term.withPushMacroExpansionStack {α : Type} (beforeStx afterStx : Syntax) (x : TermElabM α) : TermElabM α

Elaborate x with stx on the macro stack

Equations

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

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

Elaborate x with stx on the macro stack and produce macro expansion info

Equations

• Lean.Elab.Term.withMacroExpansion beforeStx afterStx x = Lean.Elab.withMacroExpansionInfo beforeStx afterStx (Lean.Elab.Term.withPushMacroExpansionStack beforeStx afterStx x)

def Lean.Elab.Term.registerSyntheticMVar (stx : Syntax) (mvarId : MVarId) (kind : SyntheticMVarKind) : TermElabM Unit

Add the given metavariable to the list of pending synthetic metavariables. The method synthesizeSyntheticMVars is used to process the metavariables on this list.

Equations

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

def Lean.Elab.Term.registerSyntheticMVarWithCurrRef (mvarId : MVarId) (kind : SyntheticMVarKind) : TermElabM Unit

Equations

• Lean.Elab.Term.registerSyntheticMVarWithCurrRef mvarId kind = do let __do_lift ← Lean.getRef Lean.Elab.Term.registerSyntheticMVar __do_lift mvarId kind

def Lean.Elab.Term.registerMVarErrorInfo (mvarErrorInfo : MVarErrorInfo) : TermElabM Unit

Equations

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

def Lean.Elab.Term.registerMVarErrorHoleInfo (mvarId : MVarId) (ref : Syntax) : TermElabM Unit

Equations

• Lean.Elab.Term.registerMVarErrorHoleInfo mvarId ref = Lean.Elab.Term.registerMVarErrorInfo { mvarId := mvarId, ref := ref, kind := Lean.Elab.Term.MVarErrorKind.hole }

def Lean.Elab.Term.registerMVarErrorImplicitArgInfo (mvarId : MVarId) (ref : Syntax) (app : Expr) : TermElabM Unit

Equations

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

def Lean.Elab.Term.registerMVarErrorCustomInfo (mvarId : MVarId) (ref : Syntax) (msgData : MessageData) : TermElabM Unit

Equations

• Lean.Elab.Term.registerMVarErrorCustomInfo mvarId ref msgData = Lean.Elab.Term.registerMVarErrorInfo { mvarId := mvarId, ref := ref, kind := Lean.Elab.Term.MVarErrorKind.custom msgData }

def Lean.Elab.Term.registerCustomErrorIfMVar (e : Expr) (ref : Syntax) (msgData : MessageData) : TermElabM Unit

Equations

• Lean.Elab.Term.registerCustomErrorIfMVar e ref msgData = match e.getAppFn with | Lean.Expr.mvar mvarId => Lean.Elab.Term.registerMVarErrorCustomInfo mvarId ref msgData | x => pure ()

def Lean.Elab.Term.registerMVarArgName (mvarId : MVarId) (argName : Name) : TermElabM Unit

Equations

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

def Lean.Elab.Term.throwMVarError {α : Type} (m : MessageData) : TermElabM α

Auxiliary method for reporting errors of the form "... contains metavariables ...". This kind of error is thrown, for example, at Match.lean where elaboration cannot continue if there are metavariables in patterns. We only want to log it if we haven't logged any errors so far.

Equations

• Lean.Elab.Term.throwMVarError m = do let __do_lift ← Lean.MonadLog.hasErrors if __do_lift = true then Lean.Elab.throwAbortTerm else Lean.throwError m

def Lean.Elab.Term.MVarErrorInfo.logError (mvarErrorInfo : MVarErrorInfo) (extraMsg? : Option MessageData) : TermElabM Unit

Equations

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

def Lean.Elab.Term.logUnassignedUsingErrorInfos (pendingMVarIds : Array MVarId) (extraMsg? : Option MessageData := none) : TermElabM Bool

Try to log errors for the unassigned metavariables pendingMVarIds.

Return true if there were "unfilled holes", and we should "abort" declaration. TODO: try to fill "all" holes using synthetic "sorry's"

Remark: We only log the "unfilled holes" as new errors if no error has been logged so far.

Equations

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

def Lean.Elab.Term.registerLevelMVarErrorInfo (levelMVarErrorInfo : LevelMVarErrorInfo) : TermElabM Unit

Equations

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

def Lean.Elab.Term.registerLevelMVarErrorExprInfo (expr : Expr) (ref : Syntax) (msgData? : Option MessageData := none) : TermElabM Unit

Equations

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

def Lean.Elab.Term.exposeLevelMVars (e : Expr) : MetaM Expr

Equations

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

def Lean.Elab.Term.LevelMVarErrorInfo.logError (levelMVarErrorInfo : LevelMVarErrorInfo) : TermElabM Unit

Equations

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

def Lean.Elab.Term.logUnassignedLevelMVarsUsingErrorInfos (pendingLevelMVarIds : Array LMVarId) : TermElabM Bool

Try to log errors for unassigned level metavariables pendingLevelMVarIds.

Returns true if there are any relevant LevelMVarErrorInfos and we should "abort" the declaration.

Remark: we only log unassigned level metavariables as new errors if no error has been logged so far.

Equations

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

def Lean.Elab.Term.ensureNoUnassignedMVars (decl : Declaration) : TermElabM Unit

Ensure metavariables registered using registerMVarErrorInfos (and used in the given declaration) have been assigned.

Equations

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

def Lean.Elab.Term.withoutPostponing {α : Type} (x : TermElabM α) : TermElabM α

Execute x without allowing it to postpone elaboration tasks. That is, tryPostpone is a noop.

Equations

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

def Lean.Elab.Term.mkExplicitBinder (ident type : Syntax) : Syntax

Creates syntax for ( <ident> : <type> )

Equations

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

def Lean.Elab.Term.levelMVarToParam (e : Expr) (except : LMVarId → Bool := fun (x : LMVarId) => false) : TermElabM Expr

Convert unassigned universe level metavariables into parameters. The new parameter names are fresh names of the form u_i with regard to ctx.levelNames, which is updated with the new names.

Equations

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

def Lean.Elab.Term.mkFreshBinderName {m : Type → Type} [Monad m] [MonadQuotation m] : m Name

Creates a fresh inaccessible binder name based on x. Equivalent to Lean.Core.mkFreshUserName `x.

Do not confuse with Lean.mkFreshId, for creating fresh free variable and metavariable ids.

Equations

• Lean.Elab.Term.mkFreshBinderName = Lean.withFreshMacroScope (Lean.MonadQuotation.addMacroScope `x)

def Lean.Elab.Term.mkFreshIdent {m : Type → Type} [Monad m] [MonadQuotation m] (ref : Syntax) (canonical : Bool := false) : m Ident

Auxiliary method for creating a Syntax.ident containing a fresh name. This method is intended for creating fresh binder names. It is just a thin layer on top of mkFreshUserName.

Equations

• Lean.Elab.Term.mkFreshIdent ref canonical = do let __do_lift ← Lean.Elab.Term.mkFreshBinderName pure (Lean.mkIdentFrom ref __do_lift canonical)

def Lean.Elab.Term.applyAttributesAt (declName : Name) (attrs : Array Attribute) (applicationTime : AttributeApplicationTime) : TermElabM Unit

Apply given attributes at a given application time

Equations

• Lean.Elab.Term.applyAttributesAt declName attrs applicationTime = Lean.Elab.Term.applyAttributesCore✝ declName attrs (some applicationTime)

def Lean.Elab.Term.applyAttributes (declName : Name) (attrs : Array Attribute) : TermElabM Unit

Equations

• Lean.Elab.Term.applyAttributes declName attrs = Lean.Elab.Term.applyAttributesCore✝ declName attrs none

def Lean.Elab.Term.mkTypeMismatchError (header? : Option MessageData) (e eType expectedType : Expr) : MetaM MessageData

Equations

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

def Lean.Elab.Term.throwTypeMismatchError {α : Type} (header? : Option MessageData) (expectedType eType e : Expr) (f? : Option Expr := none) (_extraMsg? : Option MessageData := none) : MetaM α

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Term.throwTypeMismatchError header? expectedType eType e (some f) _extraMsg? = Lean.Meta.throwAppTypeMismatch f e

def Lean.Elab.Term.withoutMacroStackAtErr {α : Type} (x : TermElabM α) : TermElabM α

Equations

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

@[reducible, inline]

abbrev Lean.Elab.Term.ContainsPendingMVar.M (α : Type) : Type

Equations

• Lean.Elab.Term.ContainsPendingMVar.M = Lean.MonadCacheT Lean.Expr Unit (OptionT Lean.MetaM)

partial def Lean.Elab.Term.ContainsPendingMVar.visit (e : Expr) : M Unit

See containsPostponedTerm

def Lean.Elab.Term.containsPendingMVar (e : Expr) : MetaM Bool

Return true if e contains a pending metavariable. Remark: it also visits let-declarations.

Equations

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

def Lean.Elab.Term.synthesizeInstMVarCore (instMVar : MVarId) (maxResultSize? : Option Nat := none) (extraErrorMsg? : Option MessageData := none) : TermElabM Bool

Try to synthesize metavariable using type class resolution. This method assumes the local context and local instances of instMVar coincide with the current local context and local instances. Return true if the instance was synthesized successfully, and false if the instance contains unassigned metavariables that are blocking the type class resolution procedure. Throw an exception if resolution or assignment irrevocably fails.

If extraErrorMsg? is not none, it contains additional information that should be attached to type class synthesis failures.

Equations

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

def Lean.Elab.Term.mkCoe (expectedType e : Expr) (f? : Option Expr := none) (errorMsgHeader? : Option String := none) (mkErrorMsg? : Option (MVarId → Expr → Expr → MetaM MessageData) := none) (mkImmedErrorMsg? : Option (Option MessageData → Expr → Expr → MetaM MessageData) := none) : TermElabM Expr

def Lean.Elab.Term.mkCoeWithErrorMsgs (expectedType e : Expr) (mkImmedErrorMsg : Option MessageData → Expr → Expr → MetaM MessageData) (mkErrorMsg : MVarId → Expr → Expr → MetaM MessageData) : TermElabM Expr

Equations

• Lean.Elab.Term.mkCoeWithErrorMsgs expectedType e mkImmedErrorMsg mkErrorMsg = Lean.Elab.Term.mkCoe expectedType e none none (some mkErrorMsg) (some mkImmedErrorMsg)

def Lean.Elab.Term.ensureHasType (expectedType? : Option Expr) (e : Expr) (errorMsgHeader? : Option String := none) (f? : Option Expr := none) : TermElabM Expr

If expectedType? is some t, then ensures t and eType are definitionally equal by inserting a coercion if necessary.

Argument f? is used only for generating error messages when inserting coercions fails.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Term.ensureHasType expectedType? e errorMsgHeader? f? = pure e

def Lean.Elab.Term.ensureHasTypeWithErrorMsgs (expectedType? : Option Expr) (e : Expr) (mkImmedErrorMsg : Option MessageData → Expr → Expr → MetaM MessageData) (mkErrorMsg : MVarId → Expr → Expr → MetaM MessageData) : TermElabM Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Term.ensureHasTypeWithErrorMsgs expectedType? e mkImmedErrorMsg mkErrorMsg = pure e

def Lean.Elab.Term.exceptionToSorry (ex : Exception) (expectedType? : Option Expr) : TermElabM Expr

Log the given exception, and create a synthetic sorry for representing the failed elaboration step with exception ex.

Equations

• Lean.Elab.Term.exceptionToSorry ex expectedType? = do Lean.Elab.logException ex Lean.Elab.Term.mkSyntheticSorryFor✝ expectedType?

def Lean.Elab.Term.tryPostpone : TermElabM Unit

If mayPostpone == true, throw Exception.postpone.

Equations

• Lean.Elab.Term.tryPostpone = do let __do_lift ← read if __do_lift.mayPostpone = true then Lean.Elab.throwPostpone else pure PUnit.unit

def Lean.Elab.Term.isMVarApp (e : Expr) : TermElabM Bool

Return true if e reduces (by unfolding only [reducible] declarations) to ?m ...

Equations

• Lean.Elab.Term.isMVarApp e = do let __do_lift ← liftM (Lean.Meta.whnfR e) pure __do_lift.getAppFn.isMVar

def Lean.Elab.Term.tryPostponeIfMVar (e : Expr) : TermElabM Unit

If mayPostpone == true and e's head is a metavariable, throw Exception.postpone.

Equations

• Lean.Elab.Term.tryPostponeIfMVar e = do let __do_lift ← Lean.Elab.Term.isMVarApp e if __do_lift = true then Lean.Elab.Term.tryPostpone else pure PUnit.unit

def Lean.Elab.Term.tryPostponeIfNoneOrMVar (e? : Option Expr) : TermElabM Unit

If e? = some e, then tryPostponeIfMVar e, otherwise it is just tryPostpone.

Equations

• Lean.Elab.Term.tryPostponeIfNoneOrMVar (some e) = Lean.Elab.Term.tryPostponeIfMVar e
• Lean.Elab.Term.tryPostponeIfNoneOrMVar none = Lean.Elab.Term.tryPostpone

def Lean.Elab.Term.tryPostponeIfHasMVars? (expectedType? : Option Expr) : TermElabM (Option Expr)

Throws Exception.postpone, if expectedType? contains unassigned metavariables. It is a noop if mayPostpone == false.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Term.tryPostponeIfHasMVars? expectedType? = do Lean.Elab.Term.tryPostponeIfNoneOrMVar expectedType? pure none

def Lean.Elab.Term.tryPostponeIfHasMVars (expectedType? : Option Expr) (msg : String) : TermElabM Expr

Throws Exception.postpone, if expectedType? contains unassigned metavariables. If mayPostpone == false, it throws error msg.

Equations

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

def Lean.Elab.Term.withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) : TermElabM Expr

Equations

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

def Lean.Elab.Term.saveContext : TermElabM SavedContext

Save relevant context for term elaboration postponement.

Equations

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

def Lean.Elab.Term.withSavedContext {α : Type} (savedCtx : SavedContext) (x : TermElabM α) : TermElabM α

Execute x with the context saved using saveContext.

Equations

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

def Lean.Elab.Term.getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDecl)

Equations

• Lean.Elab.Term.getSyntheticMVarDecl? mvarId = do let __do_lift ← get pure (Std.TreeMap.get? __do_lift.syntheticMVars mvarId)

opaque Lean.Elab.Term.debug.byAsSorry : Lean.Option Bool

def Lean.Elab.Term.mkTacticMVar (type : Expr) (tacticCode : Syntax) (kind : TacticMVarKind) (delayOnMVars : Bool := false) : TermElabM Expr

Creates a new metavariable of type type that will be synthesized using the tactic code. The tacticCode syntax is the full by .. syntax.

Equations

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

def Lean.Elab.Term.mkSaveInfoAnnotation (e : Expr) : Expr

Create an auxiliary annotation to make sure we create an Info even if e is a metavariable. See mkTermInfo.

We use this function because some elaboration functions elaborate subterms that may not be immediately part of the resulting term. Example:

let_mvar% ?m := b; wait_if_type_mvar% ?m; body

If the type of b is not known, then wait_if_type_mvar% ?m; body is postponed and just returns a fresh metavariable ?n. The elaborator for

let_mvar% ?m := b; wait_if_type_mvar% ?m; body

returns mkSaveInfoAnnotation ?n to make sure the info nodes created when elaborating b are "saved". This is a bit hackish, but elaborators like let_mvar% are rare.

Equations

• Lean.Elab.Term.mkSaveInfoAnnotation e = if e.isMVar = true then Lean.mkAnnotation `save_info e else e

def Lean.Elab.Term.isSaveInfoAnnotation? (e : Expr) : Option Expr

Equations

• Lean.Elab.Term.isSaveInfoAnnotation? e = Lean.annotation? `save_info e

partial def Lean.Elab.Term.removeSaveInfoAnnotation (e : Expr) : Expr

def Lean.Elab.Term.isTacticOrPostponedHole? (e : Expr) : TermElabM (Option MVarId)

Return some mvarId if e corresponds to a hole that is going to be filled "later" by executing a tactic or resuming elaboration.

We do not save ofTermInfo for this kind of node in the InfoTree.

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Term.isTacticOrPostponedHole? e = pure none

def Lean.Elab.Term.mkTermInfo (elaborator : Name) (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (isBinder : Bool := false) : TermElabM (Info ⊕ MVarId)

Equations

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

def Lean.Elab.Term.mkPartialTermInfo (elaborator : Name) (stx : Syntax) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) : TermElabM Info

Equations

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

def Lean.Elab.Term.addTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (elaborator : Name := Name.anonymous) (isBinder force : Bool := false) : TermElabM Expr

Pushes a new leaf node to the info tree associating the expression e to the syntax stx. As a result, when the user hovers over stx they will see the type of e, and if e is a constant they will see the constant's doc string.

• expectedType?: the expected type of e at the point of elaboration, if available
• lctx?: the local context in which to interpret e (otherwise it will use ← getLCtx)
• elaborator: a declaration name used as an alternative target for go-to-definition
• isBinder: if true, this will be treated as defining e (which should be a local constant) for the purpose of go-to-definition on local variables
• force: In patterns, the effect of addTermInfo is usually suppressed and replaced by a patternWithRef? annotation which will be turned into a term info on the post-match-elaboration expression. This flag overrides that behavior and adds the term info immediately. (See https://github.com/leanprover/lean4/pull/1664.)

Equations

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

def Lean.Elab.Term.addTermInfo' (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (elaborator : Name := Name.anonymous) (isBinder : Bool := false) : TermElabM Unit

Equations

• Lean.Elab.Term.addTermInfo' stx e expectedType? lctx? elaborator isBinder = discard (Lean.Elab.Term.addTermInfo stx e expectedType? lctx? elaborator isBinder)

def Lean.Elab.Term.withInfoContext' (stx : Syntax) (x : TermElabM Expr) (mkInfo : Expr → TermElabM (Info ⊕ MVarId)) (mkInfoOnError : TermElabM Info) : TermElabM Expr

Equations

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

structure Lean.Elab.Term.BodyInfo : Type

Info node capturing def/let rec bodies, used by the unused variables linter.

• value? : Option Expr

  The body as a fully elaborated term. none if the body failed to elaborate.

instance Lean.Elab.Term.instTypeNameBodyInfo : TypeName BodyInfo

Equations

• Lean.Elab.Term.instTypeNameBodyInfo = Lean.Elab.Term.inst✝

def Lean.Elab.Term.mkBodyInfo (stx : Syntax) (value? : Option Expr) : Info

Creates an Info.ofCustomInfo node backed by a BodyInfo.

Equations

• Lean.Elab.Term.mkBodyInfo stx value? = Lean.Elab.Info.ofCustomInfo { stx := stx, value := Dynamic.mk { value? := value? } }

def Lean.Elab.Term.getBodyInfo? : Info → Option BodyInfo

Extracts a BodyInfo custom info.

Equations

• Lean.Elab.Term.getBodyInfo? (Lean.Elab.Info.ofCustomInfo { stx := stx, value := value }) = Dynamic.get? Lean.Elab.Term.BodyInfo value
• Lean.Elab.Term.getBodyInfo? x✝ = none

def Lean.Elab.Term.withTermInfoContext' (elaborator : Name) (stx : Syntax) (x : TermElabM Expr) (expectedType? : Option Expr := none) (lctx? : Option LocalContext := none) (isBinder : Bool := false) : TermElabM Expr

Equations

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

def Lean.Elab.Term.postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : TermElabM Expr

Postpone the elaboration of stx, return a metavariable that acts as a placeholder, and ensures the info tree is updated and a hole id is introduced. When stx is elaborated, new info nodes are created and attached to the new hole id in the info tree.

Equations

• Lean.Elab.Term.postponeElabTerm stx expectedType? = Lean.Elab.Term.withTermInfoContext' Lean.Name.anonymous stx (Lean.Elab.Term.postponeElabTermCore✝ stx expectedType?) expectedType?

instance Lean.Elab.Term.instMonadMacroAdapterTermElabM : MonadMacroAdapter TermElabM

Equations

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

def Lean.Elab.Term.hasNoImplicitLambdaAnnotation (type : Expr) : Bool

Equations

• Lean.Elab.Term.hasNoImplicitLambdaAnnotation type = (Lean.annotation? `noImplicitLambda type).isSome

def Lean.Elab.Term.mkNoImplicitLambdaAnnotation (type : Expr) : Expr

Equations

• Lean.Elab.Term.mkNoImplicitLambdaAnnotation type = if Lean.Elab.Term.hasNoImplicitLambdaAnnotation type = true then type else Lean.mkAnnotation `noImplicitLambda type

def Lean.Elab.Term.blockImplicitLambda (stx : Syntax) : Bool

Block usage of implicit lambdas if stx is @f or @f arg1 ... or fun with an implicit binder annotation.

Equations

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

def Lean.Elab.Term.isLocalIdent? (stx : Syntax) : TermElabM (Option Expr)

Return true iff stx is a Syntax.ident, and it is a local variable.

Equations

• Lean.Elab.Term.isLocalIdent? (Lean.Syntax.ident info rawVal val preresolved) = do let r? ← Lean.resolveLocalName val match r? with | some (fvar, []) => pure (some fvar) | x => pure none
• Lean.Elab.Term.isLocalIdent? stx = pure none

inductive Lean.Elab.Term.UseImplicitLambdaResult : Type

• no : UseImplicitLambdaResult
• yes (expectedType : Expr) : UseImplicitLambdaResult
• postpone : UseImplicitLambdaResult

def Lean.Elab.Term.addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr) : TermElabM Unit

Store in the InfoTree that e is a "dot"-completion target. stx should cover the entire term.

Equations

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

def Lean.Elab.Term.elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone implicitLambda : Bool := true) : TermElabM Expr

Main function for elaborating terms. It extracts the elaboration methods from the environment using the node kind. Recall that the environment has a mapping from SyntaxNodeKind to TermElab methods. It creates a fresh macro scope for executing the elaboration method. All unlogged trace messages produced by the elaboration method are logged using the position information at stx. If the elaboration method throws an Exception.error and errToSorry == true, the error is logged and a synthetic sorry expression is returned. If the elaboration throws Exception.postpone and catchExPostpone == true, a new synthetic metavariable of kind SyntheticMVarKind.postponed is created, registered, and returned. The option catchExPostpone == false is used to implement resumeElabTerm to prevent the creation of another synthetic metavariable when resuming the elaboration.

If implicitLambda == false, then disable implicit lambdas feature for the given syntax, but not for its subterms. We use this flag to implement, for example, the @ modifier. If Context.implicitLambda == false, then this parameter has no effect.

Equations

• Lean.Elab.Term.elabTerm stx expectedType? catchExPostpone implicitLambda = Lean.withRef stx (Lean.Elab.Term.elabTermAux✝ expectedType? catchExPostpone implicitLambda stx)

def Lean.Elab.Term.elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone implicitLambda : Bool := true) (errorMsgHeader? : Option String := none) : TermElabM Expr

Similar to Lean.Elab.Term.elabTerm, but ensures that the type of the elaborated term is expectedType? by inserting coercions if necessary.

If errToSorry is true, then if coercion insertion fails, this function returns sorry and logs the error. Otherwise, it throws the error.

Equations

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

def Lean.Elab.Term.commitIfNoErrors? {α : Type} (x : TermElabM α) : TermElabM (Option α)

Execute x and return some if no new errors were recorded or exceptions were thrown. Otherwise, return none.

Equations

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

def Lean.Elab.Term.adaptExpander (exp : Syntax → TermElabM Syntax) : TermElab

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

Equations

• Lean.Elab.Term.adaptExpander exp stx expectedType? = do let stx' ← exp stx Lean.Elab.Term.withMacroExpansion stx stx' (Lean.Elab.Term.elabTerm stx' expectedType?)

def Lean.Elab.Term.mkInstMVar (type : Expr) (extraErrorMsg? : Option MessageData := none) : TermElabM Expr

Create a new metavariable with the given type, and try to synthesize it. If type class resolution cannot be executed (e.g., it is stuck because of metavariables in type), register metavariable as a pending one.

Equations

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

def Lean.Elab.Term.ensureType (e : Expr) : TermElabM Expr

Make sure e is a type by inferring its type and making sure it is an Expr.sort or is unifiable with Expr.sort, or can be coerced into one.

Equations

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

def Lean.Elab.Term.elabType (stx : Syntax) : TermElabM Expr

Elaborate stx and ensure result is a type.

Equations

• Lean.Elab.Term.elabType stx = do let u ← liftM Lean.Meta.mkFreshLevelMVar let type ← Lean.Elab.Term.elabTerm stx (some (Lean.mkSort u)) Lean.withRef stx (Lean.Elab.Term.ensureType type)

def Lean.Elab.Term.withAutoBoundImplicit {α : Type} (k : TermElabM α) : TermElabM α

Enable auto-bound implicits, and execute k while catching auto bound implicit exceptions. When an exception is caught, a new local declaration is created, registered, and k is tried to be executed again.

Equations

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

def Lean.Elab.Term.withoutAutoBoundImplicit {α : Type} (k : TermElabM α) : TermElabM α

Equations

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

def Lean.Elab.Term.withAutoBoundImplicitForbiddenPred {α : Type} (p : Name → Bool) (x : TermElabM α) : TermElabM α

Equations

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

def Lean.Elab.Term.collectUnassignedMVars (type : Expr) (init : Array Expr := #[]) (except : MVarId → Bool := fun (x : MVarId) => false) : TermElabM (Array Expr)

Collect unassigned metavariables in type that are not already in init and not satisfying except.

Equations

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

def Lean.Elab.Term.addAutoBoundImplicitsInlayHint (autos : Array Expr) (inlayHintPos : String.Pos) : TermElabM Unit

Adds an InlayHintInfo for the fvar auto implicits in autos at inlayHintPos. The inserted inlay hint has a hover that denotes the type of the auto-implicit (with meta-variables) and can be inserted at inlayHintPos.

Equations

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

def Lean.Elab.Term.addAutoBoundImplicits (xs : Array Expr) (inlayHintPos? : Option String.Pos) : TermElabM (Array Expr)

Return autoBoundImplicits ++ xs This method throws an error if a variable in autoBoundImplicits depends on some x in xs. The autoBoundImplicits may contain free variables created by the auto-implicit feature, and unassigned free variables. It avoids the hack used at autoBoundImplicitsOld.

If inlayHintPos? is set, this function also inserts an inlay hint denoting autoBoundImplicits. See addAutoBoundImplicitsInlayHint for more information.

Remark: we cannot simply replace every occurrence of addAutoBoundImplicitsOld with this one because a particular use-case may not be able to handle the metavariables in the array being given to k.

Equations

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

def Lean.Elab.Term.addAutoBoundImplicits' {α : Type} (xs : Array Expr) (type : Expr) (k : Array Expr → Expr → TermElabM α) (inlayHintPos? : Option String.Pos := none) : TermElabM α

Similar to addAutoBoundImplicits, but converts all metavariables into free variables.

It uses mkForallFVars + forallBoundedTelescope to convert metavariables into free variables. The type type is modified during the process if type depends on xs. We use this method to simplify the conversion of code using autoBoundImplicitsOld to autoBoundImplicits.

Equations

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

def Lean.Elab.Term.mkAuxName (suffix : Name) : TermElabM Name

Equations

• Lean.Elab.Term.mkAuxName suffix = Lean.mkAuxDeclName suffix

def Lean.Elab.Term.isLetRecAuxMVar (mvarId : MVarId) : TermElabM Bool

Return true if mvarId is an auxiliary metavariable created for compiling let rec or it is delayed assigned to one.

Equations

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

def Lean.Elab.Term.mkConst (constName : Name) (explicitLevels : List Level := []) : TermElabM Expr

Create an Expr.const using the given name and explicit levels. Remark: fresh universe metavariables are created if the constant has more universe parameters than explicitLevels.

If checkDeprecated := true, then Linter.checkDeprecated is invoked.

Equations

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

def Lean.Elab.Term.checkDeprecated (ref : Syntax) (e : Expr) : TermElabM Unit

Equations

• Lean.Elab.Term.checkDeprecated ref e = match e.getAppFn with | Lean.Expr.const declName us => Lean.withRef ref (Lean.Elab.Term.checkDeprecatedCore✝ declName) | x => pure PUnit.unit

@[inline]

def Lean.Elab.Term.withoutCheckDeprecated {m : Type → Type u_1} {α : Type} [MonadWithReaderOf Context m] : m α → m α

Equations

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

def Lean.Elab.Term.resolveName (stx : Syntax) (n : Name) (preresolved : List Syntax.Preresolved) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × List String))

Equations

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

def Lean.Elab.Term.resolveName' (ident : Syntax) (explicitLevels : List Level) (expectedType? : Option Expr := none) : TermElabM (List (Expr × Syntax × List Syntax))

Similar to resolveName, but creates identifiers for the main part and each projection with position information derived from ident. Example: Assume resolveName v.head.bla.boo produces (v.head, ["bla", "boo"]), then this method produces (v.head, id, [f₁, f₂]) where id is an identifier for v.head, and f₁ and f₂ are identifiers for fields "bla" and "boo".

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Term.resolveName' ident explicitLevels expectedType? = Lean.throwError (Lean.toMessageData "identifier expected")

def Lean.Elab.Term.resolveId? (stx : Syntax) (kind : String := "term") (withInfo : Bool := false) : TermElabM (Option Expr)

Equations

• One or more equations did not get rendered due to their size.
• Lean.Elab.Term.resolveId? stx kind withInfo = Lean.withRef stx (Lean.throwError (Lean.toMessageData "identifier expected"))

def Lean.Elab.Term.TermElabM.run {α : Type} (x : TermElabM α) (ctx : Context := { }) (s : State := { }) : MetaM (α × State)

Equations

• x.run ctx s = Lean.Meta.withConfig Lean.Elab.Term.setElabConfig ((x ctx).run s)

@[inline]

def Lean.Elab.Term.TermElabM.run' {α : Type} (x : TermElabM α) (ctx : Context := { }) (s : State := { }) : MetaM α

Equations

• x.run' ctx s = (fun (x : α × Lean.Elab.Term.State) => x.fst) <$> x.run ctx s

def Lean.Elab.Term.TermElabM.toIO {α : Type} (x : TermElabM α) (ctxCore : Core.Context) (sCore : Core.State) (ctxMeta : Meta.Context) (sMeta : Meta.State) (ctx : Context) (s : State) : IO (α × Core.State × Meta.State × State)

Equations

• x.toIO ctxCore sCore ctxMeta sMeta ctx s = do let __discr ← (x.run ctx s).toIO ctxCore sCore ctxMeta sMeta match __discr with | ((a, s), sCore, sMeta) => pure (a, sCore, sMeta, s)

def Lean.Elab.Term.universeConstraintsCheckpoint {α : Type} (x : TermElabM α) : TermElabM α

Execute x and then tries to solve pending universe constraints. Note that, stuck constraints will not be discarded.

Equations

• Lean.Elab.Term.universeConstraintsCheckpoint x = do let a ← x discard (liftM (Lean.Meta.processPostponed true true)) pure a

def Lean.Elab.Term.exprToSyntax (e : Expr) : TermElabM Term

Helper function for "embedding" an Expr in Syntax. It creates a named hole ?m and immediately assigns e to it. Examples:

let e := mkConst ``Nat.zero
`(Nat.succ $(← exprToSyntax e))

Equations

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

def Lean.Elab.withoutModifyingStateWithInfoAndMessages {m : Type → Type u_1} {α : Type} [MonadControlT TermElabM m] [Monad m] (x : m α) : m α

Equations

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