structure Lean.Elab.Term.SavedContext : Type

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

Saved context for postponed terms and tactics to be executed.

inductive Lean.Elab.Term.SyntheticMVarKind : Type

• Use typeclass resolution to synthesize value for metavariable.

  typeClass: Lean.Elab.Term.SyntheticMVarKind

• Similar to typeClass, but error messages are different. if f? is some f, we produce an application type mismatch error message. Otherwise, if header? is some header, we generate the error (header ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType) Otherwise, we generate the error ("type mismatch" ++ e ++ "has type" ++ eType ++ "but it is expected to have type" ++ expectedType)

  coe: Option String → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Option Lean.Expr → Lean.Elab.Term.SyntheticMVarKind

• Use tactic to synthesize value for metavariable.

  tactic: Lean.Syntax → Lean.Elab.Term.SavedContext → Lean.Elab.Term.SyntheticMVarKind

• Metavariable represents a hole whose elaboration has been postponed.

  postponed: Lean.Elab.Term.SavedContext → Lean.Elab.Term.SyntheticMVarKind

We use synthetic metavariables as placeholders for pending elaboration steps.

instance Lean.Elab.Term.instInhabitedSyntheticMVarKind : Inhabited Lean.Elab.Term.SyntheticMVarKind

Equations

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

instance Lean.Elab.Term.instToStringSyntheticMVarKind : ToString Lean.Elab.Term.SyntheticMVarKind

Equations

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

structure Lean.Elab.Term.SyntheticMVarDecl : Type

• stx : Lean.Syntax
• kind : Lean.Elab.Term.SyntheticMVarKind

instance Lean.Elab.Term.instInhabitedSyntheticMVarDecl : Inhabited Lean.Elab.Term.SyntheticMVarDecl

Equations

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

inductive Lean.Elab.Term.MVarErrorKind : Type

• Metavariable for implicit arguments. ctx is the parent application.

  implicitArg: Lean.Expr → Lean.Elab.Term.MVarErrorKind

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

  hole: Lean.Elab.Term.MVarErrorKind

• "Custom", msgData stores the additional error messages.

  custom: Lean.MessageData → Lean.Elab.Term.MVarErrorKind

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

instance Lean.Elab.Term.instInhabitedMVarErrorKind : Inhabited Lean.Elab.Term.MVarErrorKind

Equations

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

instance Lean.Elab.Term.instToStringMVarErrorKind : ToString Lean.Elab.Term.MVarErrorKind

Equations

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

structure Lean.Elab.Term.MVarErrorInfo : Type

• mvarId : Lean.MVarId
• ref : Lean.Syntax
• kind : Lean.Elab.Term.MVarErrorKind
• argName? : Option Lean.Name

We can optionally associate an error context with metavariables.

instance Lean.Elab.Term.instInhabitedMVarErrorInfo : Inhabited Lean.Elab.Term.MVarErrorInfo

Equations

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

structure Lean.Elab.Term.LetRecToLift : Type

• ref : Lean.Syntax
• fvarId : Lean.FVarId
• attrs : Array Lean.Elab.Attribute
• shortDeclName : Lean.Name
• declName : Lean.Name
• lctx : Lean.LocalContext
• localInstances : Lean.LocalInstances
• type : Lean.Expr
• val : Lean.Expr
• mvarId : Lean.MVarId

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

instance Lean.Elab.Term.instInhabitedLetRecToLift : Inhabited Lean.Elab.Term.LetRecToLift

Equations

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

structure Lean.Elab.Term.State : Type

• levelNames : List Lean.Name
• syntheticMVars : Lean.MVarIdMap Lean.Elab.Term.SyntheticMVarDecl
• pendingMVars : List Lean.MVarId
• mvarErrorInfos : Lean.MVarIdMap Lean.Elab.Term.MVarErrorInfo
• letRecsToLift : List Lean.Elab.Term.LetRecToLift

State of the TermElabM monad.

instance Lean.Elab.Term.instInhabitedState : Inhabited Lean.Elab.Term.State

Equations

• Lean.Elab.Term.instInhabitedState = { default := { levelNames := default, syntheticMVars := default, pendingMVars := default, mvarErrorInfos := default, letRecsToLift := default } }

structure Lean.Elab.Tactic.State : Type

• goals : List Lean.MVarId

State of the TacticM monad.

instance Lean.Elab.Tactic.instInhabitedState : Inhabited Lean.Elab.Tactic.State

Equations

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

structure Lean.Elab.Tactic.Snapshot : Type

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

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.

instance Lean.Elab.Tactic.instInhabitedSnapshot : Inhabited Lean.Elab.Tactic.Snapshot

Equations

• Lean.Elab.Tactic.instInhabitedSnapshot = { default := { core := default, meta := default, term := default, tactic := default, stx := default } }

structure Lean.Elab.Tactic.CacheKey : Type

• mvarId : Lean.MVarId
• pos : String.Pos

Key for the cache used to implement the save tactic.

instance Lean.Elab.Tactic.instBEqCacheKey : BEq Lean.Elab.Tactic.CacheKey

Equations

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

instance Lean.Elab.Tactic.instHashableCacheKey : Hashable Lean.Elab.Tactic.CacheKey

Equations

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

instance Lean.Elab.Tactic.instInhabitedCacheKey : Inhabited Lean.Elab.Tactic.CacheKey

Equations

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

structure Lean.Elab.Tactic.Cache : Type

• pre : Lean.PHashMap Lean.Elab.Tactic.CacheKey Lean.Elab.Tactic.Snapshot
• post : Lean.PHashMap Lean.Elab.Tactic.CacheKey Lean.Elab.Tactic.Snapshot

Cache for the save tactic.

instance Lean.Elab.Tactic.instInhabitedCache : Inhabited Lean.Elab.Tactic.Cache

Equations

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

structure Lean.Elab.Term.Context : Type

• declName? : Option Lean.Name

• Map .auxDecl local declarations used to encode recursive declarations to their full-names.

  auxDeclToFullName : Lean.FVarIdMap Lean.Name
• macroStack : Lean.Elab.MacroStack

• 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.

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

  errToSorry : 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 elabBinders and elabTypeWithUnboldImplicit. Both methods add implicit declarations for the unbound variable and try again.

  autoBoundImplicit : Bool
• autoBoundImplicits : Lean.PArray Lean.Expr

• 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
  

  autoBoundImplicitForbidden : Lean.Name → Bool

• Map from user name to internal unique name

  sectionVars : Lean.NameMap Lean.Name

• Map from internal name to fvar

  sectionFVars : Lean.NameMap Lean.Expr

• Enable/disable implicit lambdas feature.

  implicitLambda : Bool

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

  isNoncomputableSection : Bool

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

  ignoreTCFailures : Bool

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

  inPattern : Bool

• Cache for the save tactic. It is only some in the LSP server.

  tacticCache? : Option (IO.Ref Lean.Elab.Tactic.Cache)

• 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.

  saveRecAppSyntax : Bool

@[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)

@[inline]

abbrev Lean.Elab.Term.TermElab : Type

Equations

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

instance Lean.Elab.Term.instMonadTermElabM : Monad Lean.Elab.TermElabM

Equations

• Lean.Elab.Term.instMonadTermElabM = let i := inferInstanceAs (Monad Lean.Elab.TermElabM); Monad.mk

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

Equations

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

structure Lean.Elab.Term.SavedState : Type

• meta : Lean.Meta.SavedState
• elab : Lean.Elab.Term.State

Backtrackable state for the TermElabM monad.

instance Lean.Elab.Term.instInhabitedSavedState : Inhabited Lean.Elab.Term.SavedState

Equations

• Lean.Elab.Term.instInhabitedSavedState = { default := { meta := default, elab := default } }

def Lean.Elab.Term.saveState : Lean.Elab.TermElabM Lean.Elab.Term.SavedState

Equations

• Lean.Elab.Term.saveState = do let a ← liftM Lean.Meta.saveState let a_1 ← get pure { meta := a, elab := a_1 }

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

Equations

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

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

Equations

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

@[inline]

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

Equations

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

instance Lean.Elab.Term.instInhabitedTermElabResult {α : Type} [inst : Inhabited α] : Inhabited (Lean.Elab.Term.TermElabResult α)

Equations

• Lean.Elab.Term.instInhabitedTermElabResult = { default := EStateM.Result.ok default default }

def Lean.Elab.Term.observing {α : Type} (x : Lean.Elab.TermElabM α) : Lean.Elab.TermElabM (Lean.Elab.Term.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 : Lean.Elab.Term.TermElabResult α) : Lean.Elab.TermElabM α

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

Equations

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

def Lean.Elab.Term.commitIfDidNotPostpone {α : Type} (x : Lean.Elab.TermElabM α) : Lean.Elab.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 : Lean.Elab.TermElabM (List Lean.Name)

Return the universe level names explicitly provided by the user.

Equations

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

def Lean.Elab.Term.getFVarLocalDecl! (fvar : Lean.Expr) : Lean.Elab.TermElabM Lean.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 : Lean.AddErrorMessageContext Lean.Elab.TermElabM

Equations

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

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

Execute x but discard changes performed at Term.State and Meta.State. Recall that the Environment and InfoState 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.withoutSavingRecAppSyntax {α : Type} (x : Lean.Elab.TermElabM α) : Lean.Elab.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 : IO (Lean.KeyedDeclsAttribute Lean.Elab.Term.TermElab)

Equations

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

@[implementedBy Lean.Elab.Term.mkTermElabAttributeUnsafe]

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

opaque Lean.Elab.Term.termElabAttribute : Lean.KeyedDeclsAttribute Lean.Elab.Term.TermElab

inductive Lean.Elab.Term.LVal : Type

• fieldIdx: Lean.Syntax → Nat → Lean.Elab.Term.LVal

• Field suffix? is for producing better error messages because x.y may be a field access or a hierachical/composite name. ref is the syntax object representing the field. targetStx is the target object being accessed.

  fieldName: Lean.Syntax → String → Option Lean.Name → Lean.Syntax → Lean.Elab.Term.LVal

Auxiliary datatatype for presenting a Lean lvalue modifier. We represent a 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].

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

Equations

• Lean.Elab.Term.LVal.getRef _fun_discr = match _fun_discr with | Lean.Elab.Term.LVal.fieldIdx ref i => ref | Lean.Elab.Term.LVal.fieldName ref name suffix? targetStx => ref

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

Equations

• Lean.Elab.Term.LVal.isFieldName _fun_discr = match _fun_discr with | Lean.Elab.Term.LVal.fieldName ref name suffix? targetStx => true | x => false

instance Lean.Elab.Term.instToStringLVal : ToString Lean.Elab.Term.LVal

Equations

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

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

Return the name of the declaration being elaborated if available.

Equations

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

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

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

Equations

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

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

Return the declaration of the given metavariable

Equations

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

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

Execute x with declName? := name. See `getDeclName?

Equations

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

def Lean.Elab.Term.setLevelNames (levelNames : List Lean.Name) : Lean.Elab.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 Lean.Name) (x : Lean.Elab.TermElabM α) : Lean.Elab.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.withAuxDecl {α : Type} (shortDeclName : Lean.Name) (type : Lean.Expr) (declName : Lean.Name) (k : Lean.Expr → Lean.Elab.TermElabM α) : Lean.Elab.TermElabM α

Declare an auxiliary local declaration shortDeclName : type for elaborating recursive declaration declName, update the mapping auxDeclToFullName, and then execute k.

Equations

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

def Lean.Elab.Term.withoutErrToSorryImp {α : Type} (x : Lean.Elab.TermElabM α) : Lean.Elab.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} [inst : MonadFunctorT Lean.Elab.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 convert them into sorry applications.

Equations

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

def Lean.Elab.Term.throwErrorIfErrors : Lean.Elab.TermElabM Unit

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Term.withMacroExpansion {α : Type} (beforeStx : Lean.Syntax) (afterStx : Lean.Syntax) (x : Lean.Elab.TermElabM α) : Lean.Elab.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.registerSyntheticMVar (stx : Lean.Syntax) (mvarId : Lean.MVarId) (kind : Lean.Elab.Term.SyntheticMVarKind) : Lean.Elab.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 : Lean.MVarId) (kind : Lean.Elab.Term.SyntheticMVarKind) : Lean.Elab.TermElabM Unit

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Term.getMVarErrorInfo? (mvarId : Lean.MVarId) : Lean.Elab.TermElabM (Option Lean.Elab.Term.MVarErrorInfo)

Equations

• Lean.Elab.Term.getMVarErrorInfo? mvarId = do let a ← get pure (Lean.RBMap.find? a.mvarErrorInfos mvarId)

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

Equations

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

def Lean.Elab.Term.throwMVarError {α : Type} (m : Lean.MessageData) : Lean.Elab.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 error so far.

Equations

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

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

Equations

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

def Lean.Elab.Term.MVarErrorInfo.logError.addArgName (mvarErrorInfo : Lean.Elab.Term.MVarErrorInfo) (msg : Lean.MessageData) (extra : optParam String "") : Lean.MessageData

Append mvarErrorInfo argument name (if available) to the message. Remark: if the argument name contains macro scopes we do not append it.

Equations

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

def Lean.Elab.Term.MVarErrorInfo.logError.appendExtra (extraMsg? : Option Lean.MessageData) (msg : Lean.MessageData) : Lean.MessageData

Equations

• Lean.Elab.Term.MVarErrorInfo.logError.appendExtra extraMsg? msg = match extraMsg? with | none => msg | some extraMsg => msg ++ extraMsg

def Lean.Elab.Term.logUnassignedUsingErrorInfos (pendingMVarIds : Array Lean.MVarId) (extraMsg? : optParam (Option Lean.MessageData) none) : Lean.Elab.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.ensureNoUnassignedMVars (decl : Lean.Declaration) : Lean.Elab.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 : Lean.Elab.TermElabM α) : Lean.Elab.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 : Lean.Syntax) (type : Lean.Syntax) : Lean.Syntax

Creates syntax for ( : )

Equations

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

def Lean.Elab.Term.levelMVarToParam (e : Lean.Expr) (except : optParam (Lean.LMVarId → Bool) fun x => false) : Lean.Elab.TermElabM Lean.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} [inst : Monad m] [inst : Lean.MonadQuotation m] : m Lean.Name

Auxiliary method for creating fresh binder names. Do not confuse with the method for creating fresh free/meta variable ids.

Equations

• Lean.Elab.Term.mkFreshBinderName = Lean.withFreshMacroScope (Lean.MonadQuotation.addMacroScope (Lean.Name.mkStr1 "x"))

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

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 a ← Lean.Elab.Term.mkFreshBinderName pure (Lean.mkIdentFrom ref a canonical).raw

def Lean.Elab.Term.applyAttributesAt (declName : Lean.Name) (attrs : Array Lean.Elab.Attribute) (applicationTime : Lean.AttributeApplicationTime) : Lean.Elab.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 : Lean.Name) (attrs : Array Lean.Elab.Attribute) : Lean.Elab.TermElabM Unit

Equations

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

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

Equations

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

def Lean.Elab.Term.throwTypeMismatchError {α : Type} (header? : Option String) (expectedType : Lean.Expr) (eType : Lean.Expr) (e : Lean.Expr) (f? : optParam (Option Lean.Expr) none) (extraMsg? : optParam (Option Lean.MessageData) none) : Lean.Elab.TermElabM α

Equations

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

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

Equations

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

@[inline]

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

Equations

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

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

See containsPostponedTerm

def Lean.Elab.Term.containsPendingMVar (e : Lean.Expr) : Lean.Elab.TermElabM 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 : Lean.MVarId) (maxResultSize? : optParam (Option Nat) none) : Lean.Elab.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.

Equations

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

opaque Lean.Elab.Term.autoLift : Lean.Option Bool

opaque Lean.Elab.Term.maxCoeSize : Lean.Option Nat

def Lean.Elab.Term.synthesizeCoeInstMVarCore (instMVar : Lean.MVarId) : Lean.Elab.TermElabM Bool

Equations

• Lean.Elab.Term.synthesizeCoeInstMVarCore instMVar = do let a ← Lean.getOptions Lean.Elab.Term.synthesizeInstMVarCore instMVar (some (Lean.Option.get a Lean.Elab.Term.maxCoeSize))

def Lean.Elab.Term.tryCoeThunk? (expectedType : Lean.Expr) (eType : Lean.Expr) (e : Lean.Expr) : Lean.Elab.TermElabM (Option Lean.Expr)

The coercion from α to Thunk α cannot be implemented using an instance because it would eagerly evaluate e

Equations

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

def Lean.Elab.Term.mkCoe (expectedType : Lean.Expr) (eType : Lean.Expr) (e : Lean.Expr) (f? : optParam (Option Lean.Expr) none) (errorMsgHeader? : optParam (Option String) none) : Lean.Elab.TermElabM Lean.Expr

Equations

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

def Lean.Elab.Term.isTypeApp? (type : Lean.Expr) : Lean.Elab.TermElabM (Option (Lean.Expr × Lean.Expr))

Return some (m, α) if type can be reduced to an application of the form m α using [reducible] transparency.

Equations

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

def Lean.Elab.Term.isMonadApp (type : Lean.Expr) : Lean.Elab.TermElabM Bool

Return true if type is of the form m α where m is a Monad. Note that we reduce type using transparency [reducible].

Equations

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

def Lean.Elab.Term.ensureHasTypeAux (expectedType? : Option Lean.Expr) (eType : Lean.Expr) (e : Lean.Expr) (f? : optParam (Option Lean.Expr) none) (errorMsgHeader? : optParam (Option String) none) : Lean.Elab.TermElabM Lean.Expr

If expectedType? is some t, then ensure t and eType are definitionally equal. If they are not, then try coercions.

Argument f? is used only for generating error messages.

Equations

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

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

If expectedType? is some t, then ensure t and type of e are definitionally equal. If they are not, then try coercions.

Equations

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

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

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

Equations

• Lean.Elab.Term.exceptionToSorry ex expectedType? = do let syntheticSorry ← Lean.Elab.Term.mkSyntheticSorryFor expectedType? Lean.Elab.logException ex pure syntheticSorry

def Lean.Elab.Term.tryPostpone : Lean.Elab.TermElabM Unit

If mayPostpone == true, throw Expection.postpone.

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• Lean.Elab.Term.tryPostponeIfNoneOrMVar e? = match e? with | some e => Lean.Elab.Term.tryPostponeIfMVar e | none => Lean.Elab.Term.tryPostpone

def Lean.Elab.Term.tryPostponeIfHasMVars? (expectedType? : Option Lean.Expr) : Lean.Elab.TermElabM (Option Lean.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.

def Lean.Elab.Term.tryPostponeIfHasMVars (expectedType? : Option Lean.Expr) (msg : String) : Lean.Elab.TermElabM Lean.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.saveContext : Lean.Elab.TermElabM Lean.Elab.Term.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 : Lean.Elab.Term.SavedContext) (x : Lean.Elab.TermElabM α) : Lean.Elab.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 : Lean.MVarId) : Lean.Elab.TermElabM (Option Lean.Elab.Term.SyntheticMVarDecl)

Equations

• Lean.Elab.Term.getSyntheticMVarDecl? mvarId = do let a ← get pure (Lean.RBMap.find? a.syntheticMVars mvarId)

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

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

We use this functions 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 return 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 Lean.Expr.isMVar e = true then Lean.mkAnnotation (Lean.Name.mkStr1 "save_info") e else e

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

Equations

• Lean.Elab.Term.isSaveInfoAnnotation? e = Lean.annotation? (Lean.Name.mkStr1 "save_info") e

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

def Lean.Elab.Term.isTacticOrPostponedHole? (e : Lean.Expr) : Lean.Elab.TermElabM (Option Lean.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.

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

Equations

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

def Lean.Elab.Term.addTermInfo (stx : Lean.Syntax) (e : Lean.Expr) (expectedType? : optParam (Option Lean.Expr) none) (lctx? : optParam (Option Lean.LocalContext) none) (elaborator : optParam Lean.Name Lean.Name.anonymous) (isBinder : optParam Bool false) (force : optParam Bool false) : Lean.Elab.TermElabM Lean.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 : Lean.Syntax) (e : Lean.Expr) (expectedType? : optParam (Option Lean.Expr) none) (lctx? : optParam (Option Lean.LocalContext) none) (elaborator : optParam Lean.Name Lean.Name.anonymous) (isBinder : optParam Bool false) : Lean.Elab.TermElabM Unit

Equations

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

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

Equations

• Lean.Elab.Term.withInfoContext' stx x mkInfo = do let a ← read if a.inPattern = true then do let e ← x pure (Lean.mkPatternWithRef e stx) else Lean.Elab.withInfoContext' x mkInfo

def Lean.Elab.Term.postponeElabTerm (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) : Lean.Elab.TermElabM Lean.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

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

instance Lean.Elab.Term.instMonadMacroAdapterTermElabM : Lean.Elab.MonadMacroAdapter Lean.Elab.TermElabM

Equations

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

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

Equations

• Lean.Elab.Term.hasNoImplicitLambdaAnnotation type = Option.isSome (Lean.annotation? (Lean.Name.mkStr1 "noImplicitLambda") type)

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

Equations

• Lean.Elab.Term.mkNoImplicitLambdaAnnotation type = if Lean.Elab.Term.hasNoImplicitLambdaAnnotation type = true then type else Lean.mkAnnotation (Lean.Name.mkStr1 "noImplicitLambda") type

def Lean.Elab.Term.blockImplicitLambda (stx : Lean.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.addDotCompletionInfo (stx : Lean.Syntax) (e : Lean.Expr) (expectedType? : Option Lean.Expr) (field? : optParam (Option Lean.Syntax) none) : Lean.Elab.TermElabM Unit

Store in the InfoTree that e is a "dot"-completion target.

Equations

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

def Lean.Elab.Term.elabTerm (stx : Lean.Syntax) (expectedType? : Option Lean.Expr) (catchExPostpone : optParam Bool true) (implicitLambda : optParam Bool true) : Lean.Elab.TermElabM Lean.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 == true, 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 : Lean.Syntax) (expectedType? : Option Lean.Expr) (catchExPostpone : optParam Bool true) (implicitLambda : optParam Bool true) (errorMsgHeader? : optParam (Option String) none) : Lean.Elab.TermElabM Lean.Expr

Equations

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

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

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

Equations

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

def Lean.Elab.Term.adaptExpander (exp : Lean.Syntax → Lean.Elab.TermElabM Lean.Syntax) : Lean.Elab.Term.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? true true)

def Lean.Elab.Term.mkInstMVar (type : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Create a new metavariable with the given type, and try to synthesize it. It 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 : Lean.Expr) : Lean.Elab.TermElabM Lean.Expr

Make sure e is a type by inferring its type and making sure it is a 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 : Lean.Syntax) : Lean.Elab.TermElabM Lean.Expr

Elaborate stx and ensure result is a type.

Equations

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

def Lean.Elab.Term.withAutoBoundImplicit {α : Type} (k : Lean.Elab.TermElabM α) : Lean.Elab.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.

partial def Lean.Elab.Term.withAutoBoundImplicit.loop {α : Type} (k : Lean.Elab.TermElabM α) (s : Lean.Elab.Term.SavedState) : Lean.Elab.TermElabM α

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

Equations

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

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

Equations

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

def Lean.Elab.Term.collectUnassignedMVars (type : Lean.Expr) (init : optParam (Array Lean.Expr) #[]) (except : optParam (Lean.MVarId → Bool) fun x => false) : Lean.Elab.TermElabM (Array Lean.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.

partial def Lean.Elab.Term.collectUnassignedMVars.go (except : optParam (Lean.MVarId → Bool) fun x => false) (mvarIds : List Lean.MVarId) (result : Array Lean.Expr) : Lean.Elab.TermElabM (Array Lean.Expr)

def Lean.Elab.Term.addAutoBoundImplicits (xs : Array Lean.Expr) : Lean.Elab.TermElabM (Array Lean.Expr)

Return autoBoundImplicits ++ xs This methoid 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.

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.go (xs : Array Lean.Expr) (todo : List Lean.Expr) (autos : Array Lean.Expr) : Lean.Elab.TermElabM (Array Lean.Expr)

Equations

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

def Lean.Elab.Term.addAutoBoundImplicits' {α : Type} (xs : Array Lean.Expr) (type : Lean.Expr) (k : Array Lean.Expr → Lean.Expr → Lean.Elab.TermElabM α) : Lean.Elab.TermElabM α

Similar to autoBoundImplicits, but immediately if the resulting array of expressions contains metavariables, it immediately use mkForallFVars + forallBoundedTelescope to convert them 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 : Lean.Name) : Lean.Elab.TermElabM Lean.Name

Equations

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

def Lean.Elab.Term.isLetRecAuxMVar (mvarId : Lean.MVarId) : Lean.Elab.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.resolveLocalName (n : Lean.Name) : Lean.Elab.TermElabM (Option (Lean.Expr × List String))

Equations

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

def Lean.Elab.Term.resolveLocalName.go (localDecl : Lean.LocalDecl) (givenNameView : Lean.MacroScopesView) (fullDeclName : Lean.Name) (ns : Lean.Name) : Option Lean.LocalDecl

Equations

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

def Lean.Elab.Term.resolveLocalName.loop (view : Lean.MacroScopesView) (findLocalDecl? : Lean.MacroScopesView → Bool → Option Lean.LocalDecl) (n : Lean.Name) (projs : List String) : Option (Lean.Expr × List String)

Equations

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

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

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

Equations

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

def Lean.Elab.Term.mkConst (constName : Lean.Name) (explicitLevels : optParam (List Lean.Level) []) : Lean.Elab.TermElabM Lean.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.

Equations

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

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

Equations

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

def Lean.Elab.Term.resolveName.process (n : Lean.Name) (explicitLevels : List Lean.Level) (candidates : List (Lean.Name × List String)) : Lean.Elab.TermElabM (List (Lean.Expr × List String))

Equations

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

def Lean.Elab.Term.resolveName' (ident : Lean.Syntax) (explicitLevels : List Lean.Level) (expectedType? : optParam (Option Lean.Expr) none) : Lean.Elab.TermElabM (List (Lean.Expr × Lean.Syntax × List Lean.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.

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

Equations

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

def Lean.Elab.Term.TermElabM.run {α : Type} (x : Lean.Elab.TermElabM α) (ctx : optParam Lean.Elab.Term.Context { declName? := none, auxDeclToFullName := ∅, macroStack := [], mayPostpone := true, errToSorry := true, autoBoundImplicit := false, autoBoundImplicits := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 }, autoBoundImplicitForbidden := fun x => false, sectionVars := ∅, sectionFVars := ∅, implicitLambda := true, isNoncomputableSection := false, ignoreTCFailures := false, inPattern := false, tacticCache? := none, saveRecAppSyntax := true }) (s : optParam Lean.Elab.Term.State { levelNames := [], syntheticMVars := ∅, pendingMVars := ∅, mvarErrorInfos := ∅, letRecsToLift := [] }) : Lean.MetaM (α × Lean.Elab.Term.State)

Equations

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

@[inline]

def Lean.Elab.Term.TermElabM.run' {α : Type} (x : Lean.Elab.TermElabM α) (ctx : optParam Lean.Elab.Term.Context { declName? := none, auxDeclToFullName := ∅, macroStack := [], mayPostpone := true, errToSorry := true, autoBoundImplicit := false, autoBoundImplicits := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 }, autoBoundImplicitForbidden := fun x => false, sectionVars := ∅, sectionFVars := ∅, implicitLambda := true, isNoncomputableSection := false, ignoreTCFailures := false, inPattern := false, tacticCache? := none, saveRecAppSyntax := true }) (s : optParam Lean.Elab.Term.State { levelNames := [], syntheticMVars := ∅, pendingMVars := ∅, mvarErrorInfos := ∅, letRecsToLift := [] }) : Lean.MetaM α

Equations

• Lean.Elab.Term.TermElabM.run' x ctx s = (fun a => a.fst) <$> Lean.Elab.Term.TermElabM.run x ctx s

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

Equations

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

instance Lean.Elab.Term.instMetaEvalTermElabM {α : Type} [inst : Lean.MetaEval α] : Lean.MetaEval (Lean.Elab.TermElabM α)

Equations

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

def Lean.Elab.Term.universeConstraintsCheckpoint {α : Type} (x : Lean.Elab.TermElabM α) : Lean.Elab.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.expandDeclId (currNamespace : Lean.Name) (currLevelNames : List Lean.Name) (declId : Lean.Syntax) (modifiers : Lean.Elab.Modifiers) : Lean.Elab.TermElabM Lean.Elab.ExpandDeclIdResult

Equations

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

def Lean.Elab.Term.exprToSyntax (e : Lean.Expr) : Lean.Elab.TermElabM Lean.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} [inst : MonadControlT Lean.Elab.TermElabM m] [inst : Monad m] (x : m α) : m α

Equations

• Lean.Elab.withoutModifyingStateWithInfoAndMessages x = controlAt Lean.Elab.TermElabM fun runInBase => Lean.Elab.Term.withoutModifyingStateWithInfoAndMessagesImpl (runInBase x)