This module provides four (mutually dependent) goodies that are needed for building the elaborator and tactic frameworks. 1- Weak head normal form computation with support for metavariables and transparency modes. 2- Definitionally equality checking with support for metavariables (aka unification modulo definitional equality). 3- Type inference. 4- Type class resolution.

They are packed into the MetaM monad.

opaque Lean.Meta.isDefEqStuckExceptionId : InternalExceptionId

def Lean.Meta.TransparencyMode.toUInt64 : TransparencyMode → UInt64

Equations

• Lean.Meta.TransparencyMode.all.toUInt64 = 0
• Lean.Meta.TransparencyMode.default.toUInt64 = 1
• Lean.Meta.TransparencyMode.reducible.toUInt64 = 2
• Lean.Meta.TransparencyMode.instances.toUInt64 = 3

def Lean.Meta.EtaStructMode.toUInt64 : EtaStructMode → UInt64

Equations

• Lean.Meta.EtaStructMode.all.toUInt64 = 0
• Lean.Meta.EtaStructMode.notClasses.toUInt64 = 1
• Lean.Meta.EtaStructMode.none.toUInt64 = 2

inductive Lean.Meta.ProjReductionKind : Type

Configuration for projection reduction. See whnfCore.

• no : ProjReductionKind

  Projections s.i are not reduced at whnfCore.

• yes : ProjReductionKind

  Projections s.i are reduced at whnfCore, and whnfCore is used at s during the process. Recall that whnfCore does not perform delta reduction (i.e., it will not unfold constant declarations).

• yesWithDelta : ProjReductionKind

  Projections s.i are reduced at whnfCore, and whnf is used at s during the process. Recall that whnfCore does not perform delta reduction (i.e., it will not unfold constant declarations), but whnf does.

• yesWithDeltaI : ProjReductionKind

  Projections s.i are reduced at whnfCore, and whnfAtMostI is used at s during the process. Recall that whnfAtMostI is like whnf but uses transparency at most instances. This option is stronger than yes, but weaker than yesWithDelta. We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations. When unifying e.g. (@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1, we only want to unify negation (and not all other field operations as well). Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986

instance Lean.Meta.instDecidableEqProjReductionKind : DecidableEq ProjReductionKind

Equations

• Lean.Meta.instDecidableEqProjReductionKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Lean.Meta.instInhabitedProjReductionKind.default : ProjReductionKind

Equations

• Lean.Meta.instInhabitedProjReductionKind.default = Lean.Meta.ProjReductionKind.no

instance Lean.Meta.instInhabitedProjReductionKind : Inhabited ProjReductionKind

Equations

• Lean.Meta.instInhabitedProjReductionKind = { default := Lean.Meta.instInhabitedProjReductionKind.default }

def Lean.Meta.instReprProjReductionKind.repr : ProjReductionKind → Nat → Format

Equations

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

instance Lean.Meta.instReprProjReductionKind : Repr ProjReductionKind

Equations

• Lean.Meta.instReprProjReductionKind = { reprPrec := Lean.Meta.instReprProjReductionKind.repr }

def Lean.Meta.ProjReductionKind.toUInt64 : ProjReductionKind → UInt64

Equations

• Lean.Meta.ProjReductionKind.no.toUInt64 = 0
• Lean.Meta.ProjReductionKind.yes.toUInt64 = 1
• Lean.Meta.ProjReductionKind.yesWithDelta.toUInt64 = 2
• Lean.Meta.ProjReductionKind.yesWithDeltaI.toUInt64 = 3

structure Lean.Meta.Config : Type

Configuration flags for the MetaM monad. Many of them are used to control the isDefEq function that checks whether two terms are definitionally equal or not. Recall that when isDefEq is trying to check whether ?m@C a₁ ... aₙ and t are definitionally equal (?m@C a₁ ... aₙ =?= t), where ?m@C as a shorthand for C |- ?m : t where t is the type of ?m. We solve it using the assignment ?m := fun a₁ ... aₙ => t if

1. a₁ ... aₙ are pairwise distinct free variables that are ​not​ let-variables.
2. a₁ ... aₙ are not in C
3. t only contains free variables in C and/or {a₁, ..., aₙ}
4. For every metavariable ?m'@C' occurring in t, C' is a subprefix of C
5. ?m does not occur in t

• foApprox : Bool

  If foApprox is set to true, and some aᵢ is not a free variable, then we use first-order unification

    ?m a_1 ... a_i a_{i+1} ... a_{i+k} =?= f b_1 ... b_k
  

  reduces to

    ?m a_1 ... a_i =?= f
    a_{i+1}        =?= b_1
    ...
    a_{i+k}        =?= b_k
  

• ctxApprox : Bool

  When ctxApprox is set to true, we relax condition 4, by creating an auxiliary metavariable ?n' with a smaller context than ?m'.

• quasiPatternApprox : Bool

  When quasiPatternApprox is set to true, we ignore condition 2.

• constApprox : Bool

  When constApprox is set to true, we solve ?m t =?= c using ?m := fun _ => c when ?m t is not a higher-order pattern and c is not an application as

• isDefEqStuckEx : Bool

  When the following flag is set, isDefEq throws the exception Exception.isDefEqStuck whenever it encounters a constraint ?m ... =?= t where ?m is read only. This feature is useful for type class resolution where we may want to notify the caller that the TC problem may be solvable later after it assigns ?m.

• unificationHints : Bool

  Enable/disable the unification hints feature.

• proofIrrelevance : Bool

  Enables proof irrelevance at isDefEq

• assignSyntheticOpaque : Bool

  By default synthetic opaque metavariables are not assigned by isDefEq. Motivation: we want to make sure typing constraints resolved during elaboration should not "fill" holes that are supposed to be filled using tactics. However, this restriction is too restrictive for tactics such as exact t. When elaborating t, we dot not fill named holes when solving typing constraints or TC resolution. But, we ignore the restriction when we try to unify the type of t with the goal target type. We claim this is not a hack and is defensible behavior because this last unification step is not really part of the term elaboration.

• offsetCnstrs : Bool

  Enable/Disable support for offset constraints such as ?x + 1 =?= e

• transparency : TransparencyMode

  Controls which definitions and theorems can be unfolded by isDefEq and whnf.

• etaStruct : EtaStructMode

  Eta for structures configuration mode.

• univApprox : Bool

  When univApprox is set to true, we use approximations when solving postponed universe constraints. Examples:

  • max u ?v =?= u is solved with ?v := u and ignoring the solution ?v := 0.
  • max u w =?= max u ?v is solved with ?v := w ignoring the solution ?v := max u w
• iota : Bool

  If true, reduce recursor/matcher applications, e.g., Nat.rec true (fun _ _ => false) Nat.zero reduces to true

• beta : Bool

  If true, reduce terms such as (fun x => t[x]) a into t[a]

• proj : ProjReductionKind

  Control projection reduction at whnfCore.

• zeta : Bool

  Zeta reduction: let x := v; e[x] and have x := v; e[x] reduce to e[v]. We say a let-declaration let x := v; e is nondependent if it is equivalent to (fun x => e) v. Recall that

  fun x : BitVec 5 => let n := 5; fun y : BitVec n => x = y
  

  is type correct, but

  fun x : BitVec 5 => (fun n => fun y : BitVec n => x = y) 5
  

  is not. See also zetaHave, for disabling the reduction nondependent lets (have expressions).

• zetaDelta : Bool

  Zeta-delta reduction: given a local context containing entry x : t := e, free variable x reduces to e.

• zetaUnused : Bool

  Zeta reduction for unused let-declarations: let x := v; e reduces to e when x does not occur in e. This option takes precedence over zeta and zetaHave.

• zetaHave : Bool

  When zeta := true, then zetaHave := false disables zeta reduction of have expressions.

def Lean.Meta.instInhabitedConfig.default : Config

Equations

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

instance Lean.Meta.instInhabitedConfig : Inhabited Config

Equations

• Lean.Meta.instInhabitedConfig = { default := Lean.Meta.instInhabitedConfig.default }

instance Lean.Meta.instReprConfig_2 : Repr Config

Equations

• Lean.Meta.instReprConfig_2 = { reprPrec := Lean.Meta.instReprConfig_2.repr }

def Lean.Meta.instReprConfig_2.repr : Config → Nat → Format

Equations

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

structure Lean.Meta.ConfigWithKey : Type

Configuration with key produced by Config.toKey.

• config : Config
• key : UInt64

instance Lean.Meta.instInhabitedConfigWithKey : Inhabited ConfigWithKey

Equations

• Lean.Meta.instInhabitedConfigWithKey = { default := Lean.Meta.instInhabitedConfigWithKey._private_1 }

def Lean.Meta.Config.toConfigWithKey (c : Config) : ConfigWithKey

Equations

• c.toConfigWithKey = { config := c }

structure Lean.Meta.ParamInfo : Type

Function parameter information cache.

• binderInfo : BinderInfo

  The binder annotation for the parameter.

• hasFwdDeps : Bool

  hasFwdDeps is true if there is another parameter whose type depends on this one.

• backDeps : Array Nat

  backDeps contains the backwards dependencies. That is, the (0-indexed) position of previous parameters that this one depends on.

• isProp : Bool

  isProp is true if the parameter type is always a proposition.

• isDecInst : Bool

  isDecInst is true if the parameter's type is of the form Decidable .... This information affects the generation of congruence theorems.

• higherOrderOutParam : Bool

  higherOrderOutParam is true if this parameter is a higher-order output parameter of local instance. Example:

  getElem :
    {cont : Type u_1} → {idx : Type u_2} → {elem : Type u_3} →
    {dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] →
    (xs : cont) → (i : idx) → dom xs i → elem
  

  This flag is true for the parameter dom because it is output parameter of [self : GetElem cont idx elem dom]

• dependsOnHigherOrderOutParam : Bool

  dependsOnHigherOrderOutParam is true if the type of this parameter depends on the higher-order output parameter of a previous local instance. Example:

  getElem :
    {cont : Type u_1} → {idx : Type u_2} → {elem : Type u_3} →
    {dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] →
    (xs : cont) → (i : idx) → dom xs i → elem
  

  This flag is true for the parameter with type dom xs i since dom is an output parameter of the instance [self : GetElem cont idx elem dom]

def Lean.Meta.instInhabitedParamInfo.default : ParamInfo

Equations

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

instance Lean.Meta.instInhabitedParamInfo : Inhabited ParamInfo

Equations

• Lean.Meta.instInhabitedParamInfo = { default := Lean.Meta.instInhabitedParamInfo.default }

def Lean.Meta.ParamInfo.isImplicit (p : ParamInfo) : Bool

Equations

• p.isImplicit = (p.binderInfo == Lean.BinderInfo.implicit)

def Lean.Meta.ParamInfo.isInstImplicit (p : ParamInfo) : Bool

Equations

• p.isInstImplicit = (p.binderInfo == Lean.BinderInfo.instImplicit)

def Lean.Meta.ParamInfo.isStrictImplicit (p : ParamInfo) : Bool

Equations

• p.isStrictImplicit = (p.binderInfo == Lean.BinderInfo.strictImplicit)

def Lean.Meta.ParamInfo.isExplicit (p : ParamInfo) : Bool

Equations

• p.isExplicit = (p.binderInfo == Lean.BinderInfo.default)

structure Lean.Meta.FunInfo : Type

Function information cache. See ParamInfo.

• paramInfo : Array ParamInfo

  Parameter information cache.

• resultDeps : Array Nat

  resultDeps contains the function result type backwards dependencies. That is, the (0-indexed) position of parameters that the result type depends on.

instance Lean.Meta.instTypeNameFunInfo : TypeName FunInfo

Equations

• Lean.Meta.instTypeNameFunInfo = Lean.Meta.inst✝

structure Lean.Meta.InfoCacheKey : Type

Key for the function information cache.

• configKey : UInt64

  key produced using Config.toKey.

• expr : Expr

  The function being cached information about. It is quite often an Expr.const.

• nargs? : Option Nat

  nargs? = some n if the cached information was computed assuming the function has arity n. If nargs? = none, then the cache information consumed the arrow type as much as possible using the current transparency setting. X

def Lean.Meta.instInhabitedInfoCacheKey.default : InfoCacheKey

Equations

• Lean.Meta.instInhabitedInfoCacheKey.default = { configKey := default, expr := default, nargs? := default }

instance Lean.Meta.instInhabitedInfoCacheKey : Inhabited InfoCacheKey

Equations

• Lean.Meta.instInhabitedInfoCacheKey = { default := Lean.Meta.instInhabitedInfoCacheKey.default }

def Lean.Meta.instBEqInfoCacheKey.beq : InfoCacheKey → InfoCacheKey → Bool

Equations

• Lean.Meta.instBEqInfoCacheKey.beq { configKey := a, expr := a_1, nargs? := a_2 } { configKey := b, expr := b_1, nargs? := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.Meta.instBEqInfoCacheKey.beq x✝¹ x✝ = false

instance Lean.Meta.instBEqInfoCacheKey : BEq InfoCacheKey

Equations

• Lean.Meta.instBEqInfoCacheKey = { beq := Lean.Meta.instBEqInfoCacheKey.beq }

instance Lean.Meta.instHashableInfoCacheKey : Hashable InfoCacheKey

Equations

• Lean.Meta.instHashableInfoCacheKey = { hash := Lean.Meta.instHashableInfoCacheKey._private_1 }

structure Lean.Meta.SynthInstanceCacheKey : Type

• localInsts : LocalInstances
• type : Expr
• synthPendingDepth : Nat

  Value of synthPendingDepth when instance was synthesized or failed to be synthesized. See issue #2522.

instance Lean.Meta.instHashableSynthInstanceCacheKey : Hashable SynthInstanceCacheKey

Equations

• Lean.Meta.instHashableSynthInstanceCacheKey = { hash := Lean.Meta.instHashableSynthInstanceCacheKey.hash }

def Lean.Meta.instHashableSynthInstanceCacheKey.hash : SynthInstanceCacheKey → UInt64

Equations

• Lean.Meta.instHashableSynthInstanceCacheKey.hash { localInsts := a, type := a_1, synthPendingDepth := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

def Lean.Meta.instBEqSynthInstanceCacheKey.beq : SynthInstanceCacheKey → SynthInstanceCacheKey → Bool

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.instBEqSynthInstanceCacheKey.beq x✝¹ x✝ = false

instance Lean.Meta.instBEqSynthInstanceCacheKey : BEq SynthInstanceCacheKey

Equations

• Lean.Meta.instBEqSynthInstanceCacheKey = { beq := Lean.Meta.instBEqSynthInstanceCacheKey.beq }

structure Lean.Meta.AbstractMVarsResult : Type

Resulting type for abstractMVars

• paramNames : Array Name
• mvars : Array Expr
• expr : Expr

instance Lean.Meta.instInhabitedAbstractMVarsResult : Inhabited AbstractMVarsResult

Equations

• Lean.Meta.instInhabitedAbstractMVarsResult = { default := Lean.Meta.instInhabitedAbstractMVarsResult.default }

def Lean.Meta.instInhabitedAbstractMVarsResult.default : AbstractMVarsResult

Equations

• Lean.Meta.instInhabitedAbstractMVarsResult.default = { paramNames := default, mvars := default, expr := default }

def Lean.Meta.instBEqAbstractMVarsResult.beq : AbstractMVarsResult → AbstractMVarsResult → Bool

Equations

• Lean.Meta.instBEqAbstractMVarsResult.beq { paramNames := a, mvars := a_1, expr := a_2 } { paramNames := b, mvars := b_1, expr := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.Meta.instBEqAbstractMVarsResult.beq x✝¹ x✝ = false

instance Lean.Meta.instBEqAbstractMVarsResult : BEq AbstractMVarsResult

Equations

• Lean.Meta.instBEqAbstractMVarsResult = { beq := Lean.Meta.instBEqAbstractMVarsResult.beq }

def Lean.Meta.AbstractMVarsResult.numMVars (r : AbstractMVarsResult) : Nat

Equations

• r.numMVars = r.mvars.size

@[reducible, inline]

abbrev Lean.Meta.SynthInstanceCache : Type

Equations

• Lean.Meta.SynthInstanceCache = Lean.PersistentHashMap Lean.Meta.SynthInstanceCacheKey (Option Lean.Meta.AbstractMVarsResult)

structure Lean.Meta.ExprConfigCacheKey : Type

• expr : Expr
• configKey : UInt64

instance Lean.Meta.instInhabitedExprConfigCacheKey : Inhabited ExprConfigCacheKey

Equations

• Lean.Meta.instInhabitedExprConfigCacheKey = { default := Lean.Meta.instInhabitedExprConfigCacheKey.default }

def Lean.Meta.instInhabitedExprConfigCacheKey.default : ExprConfigCacheKey

Equations

• Lean.Meta.instInhabitedExprConfigCacheKey.default = { expr := default, configKey := default }

instance Lean.Meta.instBEqExprConfigCacheKey : BEq ExprConfigCacheKey

Equations

• Lean.Meta.instBEqExprConfigCacheKey = { beq := fun (a b : Lean.Meta.ExprConfigCacheKey) => a.expr.equal b.expr && a.configKey == b.configKey }

instance Lean.Meta.instHashableExprConfigCacheKey : Hashable ExprConfigCacheKey

Equations

• Lean.Meta.instHashableExprConfigCacheKey = { hash := Lean.Meta.instHashableExprConfigCacheKey._private_1 }

@[reducible, inline]

abbrev Lean.Meta.InferTypeCache : Type

Equations

• Lean.Meta.InferTypeCache = Lean.PersistentHashMap Lean.Meta.ExprConfigCacheKey Lean.Expr

@[reducible, inline]

abbrev Lean.Meta.FunInfoCache : Type

Equations

• Lean.Meta.FunInfoCache = Lean.PersistentHashMap Lean.Meta.InfoCacheKey Lean.Meta.FunInfo

@[reducible, inline]

abbrev Lean.Meta.WhnfCache : Type

Equations

• Lean.Meta.WhnfCache = Lean.PersistentHashMap Lean.Meta.ExprConfigCacheKey Lean.Expr

structure Lean.Meta.DefEqCacheKey : Type

• lhs : Expr
• rhs : Expr
• configKey : UInt64

def Lean.Meta.instInhabitedDefEqCacheKey.default : DefEqCacheKey

Equations

• Lean.Meta.instInhabitedDefEqCacheKey.default = { lhs := default, rhs := default, configKey := default }

instance Lean.Meta.instInhabitedDefEqCacheKey : Inhabited DefEqCacheKey

Equations

• Lean.Meta.instInhabitedDefEqCacheKey = { default := Lean.Meta.instInhabitedDefEqCacheKey.default }

instance Lean.Meta.instBEqDefEqCacheKey : BEq DefEqCacheKey

Equations

• Lean.Meta.instBEqDefEqCacheKey = { beq := Lean.Meta.instBEqDefEqCacheKey.beq }

def Lean.Meta.instBEqDefEqCacheKey.beq : DefEqCacheKey → DefEqCacheKey → Bool

Equations

• Lean.Meta.instBEqDefEqCacheKey.beq { lhs := a, rhs := a_1, configKey := a_2 } { lhs := b, rhs := b_1, configKey := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Lean.Meta.instBEqDefEqCacheKey.beq x✝¹ x✝ = false

instance Lean.Meta.instHashableDefEqCacheKey : Hashable DefEqCacheKey

Equations

• Lean.Meta.instHashableDefEqCacheKey = { hash := Lean.Meta.instHashableDefEqCacheKey._private_1 }

@[reducible, inline]

abbrev Lean.Meta.DefEqCache : Type

A mapping (s, t) ↦ isDefEq s t. TODO: consider more efficient representations (e.g., a proper set) and caching policies (e.g., imperfect cache). We should also investigate the impact on memory consumption.

Equations

• Lean.Meta.DefEqCache = Lean.PersistentHashMap Lean.Meta.DefEqCacheKey Bool

structure Lean.Meta.Cache : Type

Cache datastructures for type inference, type class resolution, whnf, and definitional equality.

• inferType : InferTypeCache
• funInfo : FunInfoCache
• synthInstance : SynthInstanceCache
• whnf : WhnfCache
• defEqTrans : DefEqCache
• defEqPerm : DefEqCache

def Lean.Meta.instInhabitedCache.default : Cache

Equations

• Lean.Meta.instInhabitedCache.default = { inferType := default, funInfo := default, synthInstance := default, whnf := default, defEqTrans := default, defEqPerm := default }

instance Lean.Meta.instInhabitedCache : Inhabited Cache

Equations

• Lean.Meta.instInhabitedCache = { default := Lean.Meta.instInhabitedCache.default }

structure Lean.Meta.DefEqContext : Type

"Context" for a postponed universe constraint. lhs and rhs are the surrounding isDefEq call when the postponed constraint was created.

• lhs : Expr
• rhs : Expr
• lctx : LocalContext
• localInstances : LocalInstances

structure Lean.Meta.PostponedEntry : Type

Auxiliary structure for representing postponed universe constraints. Remark: the fields ref and rootDefEq? are used for error message generation only. Remark: we may consider improving the error message generation in the future.

• ref : Syntax

  We save the ref at entry creation time. This is used for reporting errors back to the user.

• lhs : Level
• rhs : Level
• ctx? : Option DefEqContext

  Context for the surrounding isDefEq call when the entry was created.

instance Lean.Meta.instInhabitedPostponedEntry : Inhabited PostponedEntry

Equations

• Lean.Meta.instInhabitedPostponedEntry = { default := Lean.Meta.instInhabitedPostponedEntry.default }

def Lean.Meta.instInhabitedPostponedEntry.default : PostponedEntry

Equations

• Lean.Meta.instInhabitedPostponedEntry.default = { ref := default, lhs := default, rhs := default, ctx? := default }

structure Lean.Meta.Diagnostics : Type

• unfoldCounter : PHashMap Name Nat

  Number of times each declaration has been unfolded

• heuristicCounter : PHashMap Name Nat

  Number of times f a =?= f b heuristic has been used per function f.

• instanceCounter : PHashMap Name Nat

  Number of times a TC instance is used.

• synthPendingFailures : PHashMap Expr MessageData

  Pending instances that were not synthesized because maxSynthPendingDepth has been reached.

def Lean.Meta.instInhabitedDiagnostics.default : Diagnostics

Equations

• Lean.Meta.instInhabitedDiagnostics.default = { unfoldCounter := default, heuristicCounter := default, instanceCounter := default, synthPendingFailures := default }

instance Lean.Meta.instInhabitedDiagnostics : Inhabited Diagnostics

Equations

• Lean.Meta.instInhabitedDiagnostics = { default := Lean.Meta.instInhabitedDiagnostics.default }

structure Lean.Meta.State : Type

MetaM monad state.

• mctx : MetavarContext
• cache : Cache
• zetaDeltaFVarIds : FVarIdSet

  When Context.trackZetaDelta == true, then any let-decl free variable that is zetaDelta-expanded by MetaM is stored in zetaDeltaFVarIds.

• postponed : PersistentArray PostponedEntry

  Array of postponed universe level constraints

• diag : Diagnostics

instance Lean.Meta.instInhabitedState : Inhabited State

Equations

• Lean.Meta.instInhabitedState = { default := Lean.Meta.instInhabitedState.default }

def Lean.Meta.instInhabitedState.default : State

Equations

• Lean.Meta.instInhabitedState.default = { mctx := default, cache := default, zetaDeltaFVarIds := default, postponed := default, diag := default }

structure Lean.Meta.SavedState : Type

Backtrackable state for the MetaM monad.

• core : Core.SavedState
• meta : State

instance Lean.Meta.instNonemptySavedState : Nonempty SavedState

opaque Lean.Meta.maxSynthPendingDepth : Lean.Option Nat

structure Lean.Meta.Context : Type

Contextual information for the MetaM monad.

• keyedConfig : ConfigWithKey
• trackZetaDelta : Bool

  When trackZetaDelta = true, we track all free variables that have been zetaDelta-expanded. That is, suppose the local context contains the declaration x : t := v, and we reduce x to v, then we insert x into State.zetaDeltaFVarIds. We use trackZetaDelta to discover which let-declarations let x := v; e can be represented as have x := v; e. When we find these declarations we set their nondep flag with true. To find these let-declarations in a given term s, we 1- Reset State.zetaDeltaFVarIds 2- Set trackZetaDelta := true 3- Type-check s.

  Note that, we do not include this field in the Config structure because this field is not taken into account while caching results. See also field zetaDeltaSet.

• zetaDeltaSet : FVarIdSet

  If config.zetaDelta := false, we may select specific local declarations to be unfolded using the field zetaDeltaSet. Note that, we do not include this field in the Config structure because this field is not taken into account while caching results. Moreover, we reset all caches whenever setting it.

• lctx : LocalContext

  Local context

• localInstances : LocalInstances

  Local instances in lctx.

• defEqCtx? : Option DefEqContext

  Not none when inside of an isDefEq test. See PostponedEntry.

• synthPendingDepth : Nat

  Track the number of nested synthPending invocations. Nested invocations can happen when the type class resolution invokes synthPending.

  Remark: synthPending fails if synthPendingDepth > maxSynthPendingDepth.

• canUnfold? : Option (Config → ConstantInfo → CoreM Bool)

  A predicate to control whether a constant can be unfolded or not at whnf. Note that we do not cache results at whnf when canUnfold? is not none.

• univApprox : Bool

  When Config.univApprox := true, this flag is set to true when there is no progress processing universe constraints.

• inTypeClassResolution : Bool

  inTypeClassResolution := true when isDefEq is invoked at tryResolve in the type class resolution module. We don't use isDefEqProjDelta when performing TC resolution due to performance issues. This is not a great solution, but a proper solution would require a more sophisticated caching mechanism.

instance Lean.Meta.instInhabitedContext : Inhabited Context

Equations

• Lean.Meta.instInhabitedContext = { default := Lean.Meta.instInhabitedContext.default }

def Lean.Meta.instInhabitedContext.default : Context

Equations

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

def Lean.Meta.Context.config (c : Context) : Config

Equations

• c.config = c.keyedConfig.config

def Lean.Meta.Context.configKey (c : Context) : UInt64

Equations

• c.configKey = c.keyedConfig.key

@[reducible, inline]

abbrev Lean.Meta.MetaM (α : Type) : Type

The MetaM monad is a core component of Lean's metaprogramming framework, facilitating the construction and manipulation of expressions (Lean.Expr) within Lean.

It builds on top of CoreM and additionally provides:

• A LocalContext for managing free variables.
• A MetavarContext for managing metavariables.
• A Cache for caching results of the key MetaM operations.

The key operations provided by MetaM are:

• inferType, which attempts to automatically infer the type of a given expression.
• whnf, which reduces an expression to the point where the outermost part is no longer reducible but the inside may still contain unreduced expression.
• isDefEq, which determines whether two expressions are definitionally equal, possibly assigning meta variables in the process.
• forallTelescope and lambdaTelescope, which make it possible to automatically move into (nested) binders while updating the local context.

The following is a small example that demonstrates how to obtain and manipulate the type of a Fin expression:

public import Lean

open Lean Meta

def getFinBound (e : Expr) : MetaM (Option Expr) := do
  let type ← whnf (← inferType e)
  let_expr Fin bound := type | return none
  return bound

def a : Fin 100 := 42

run_meta
  match ← getFinBound (.const ``a []) with
  | some limit => IO.println (← ppExpr limit)
  | none => IO.println "no limit found"

Equations

• Lean.MetaM = ReaderT Lean.Meta.Context (StateRefT' IO.RealWorld Lean.Meta.State Lean.CoreM)

@[always_inline]

instance Lean.Meta.instMonadMetaM : Monad MetaM

Equations

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

instance Lean.Meta.instInhabitedMetaM {α : Type} : Inhabited (MetaM α)

Equations

• Lean.Meta.instInhabitedMetaM = { default := fun (x : Lean.Meta.Context) (x : ST.Ref IO.RealWorld Lean.Meta.State) => default }

instance Lean.Meta.instMonadLCtxMetaM : MonadLCtx MetaM

Equations

• Lean.Meta.instMonadLCtxMetaM = { getLCtx := do let __do_lift ← read pure __do_lift.lctx }

instance Lean.Meta.instMonadMCtxMetaM : MonadMCtx MetaM

Equations

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

instance Lean.Meta.instMonadEnvMetaM : MonadEnv MetaM

Equations

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

instance Lean.Meta.instAddMessageContextMetaM : AddMessageContext MetaM

Equations

• Lean.Meta.instAddMessageContextMetaM = { addMessageContext := Lean.addMessageContextFull }

def Lean.Meta.saveState : MetaM SavedState

Equations

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

def Lean.Meta.SavedState.restore (b : SavedState) : MetaM Unit

Restore backtrackable parts of the state.

Equations

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

@[specialize #[]]

def Lean.Meta.withRestoreOrSaveFull {α : Type} (reusableResult? : Option (α × SavedState)) (act : MetaM α) : MetaM (α × SavedState)

Incremental reuse primitive: if reusableResult? is none, runs act and returns its result together with the saved monadic state after act including the heartbeats used by it. If reusableResult? on the other hand is some (a, state), restores full state including heartbeats used and returns (a, state).

The intention is for steps that support incremental reuse to initially pass none as reusableResult? and store the result and state in a snapshot. In a further run, if reuse is possible, reusableResult? should be set to the previous result and state, ensuring that the state after running withRestoreOrSaveFull is identical in both runs. Note however that necessarily this is only an approximation in the case of heartbeats as heartbeats used by withRestoreOrSaveFull itself after calling act as well as by reuse-handling code such as the one supplying reusableResult? are not accounted for.

Equations

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

instance Lean.Meta.instMonadBacktrackSavedStateMetaM : MonadBacktrack SavedState MetaM

Equations

• Lean.Meta.instMonadBacktrackSavedStateMetaM = { saveState := Lean.Meta.saveState, restoreState := fun (s : Lean.Meta.SavedState) => s.restore }

@[inline]

def Lean.Meta.MetaM.run {α : Type} (x : MetaM α) (ctx : Context := { }) (s : State := { }) : CoreM (α × State)

Equations

• x.run ctx s = (x ctx).run s

@[inline]

def Lean.Meta.MetaM.run' {α : Type} (x : MetaM α) (ctx : Context := { }) (s : State := { }) : CoreM α

Equations

• x.run' ctx s = Prod.fst <$> x.run ctx s

@[inline]

def Lean.Meta.MetaM.toIO {α : Type} (x : MetaM α) (ctxCore : Core.Context) (sCore : Core.State) (ctx : Context := { }) (s : State := { }) : IO (α × Core.State × State)

Equations

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

def Lean.Meta.throwIsDefEqStuck {α : Type} : MetaM α

Equations

• Lean.Meta.throwIsDefEqStuck = throw (Lean.Exception.internal Lean.Meta.isDefEqStuckExceptionId)

@[inline]

def Lean.Meta.liftMetaM {m : Type → Type u_1} {α : Type} [MonadLiftT MetaM m] (x : MetaM α) : m α

Equations

• Lean.Meta.liftMetaM x = liftM x

@[inline]

def Lean.Meta.mapMetaM {m : Type → Type u_1} [MonadControlT MetaM m] [Monad m] (f : {α : Type} → MetaM α → MetaM α) {α : Type} (x : m α) : m α

Equations

• Lean.Meta.mapMetaM f x = controlAt Lean.MetaM fun (runInBase : {β : Type} → m β → Lean.MetaM (stM Lean.MetaM m β)) => f (runInBase x)

@[inline]

def Lean.Meta.map1MetaM {m : Type → Type u_1} {β : Sort u_2} [MonadControlT MetaM m] [Monad m] (f : {α : Type} → (β → MetaM α) → MetaM α) {α : Type} (k : β → m α) : m α

Equations

• Lean.Meta.map1MetaM f k = controlAt Lean.MetaM fun (runInBase : {β : Type} → m β → Lean.MetaM (stM Lean.MetaM m β)) => f fun (b : β) => runInBase (k b)

@[inline]

def Lean.Meta.map2MetaM {m : Type → Type u_1} {β : Sort u_2} {γ : Sort u_3} [MonadControlT MetaM m] [Monad m] (f : {α : Type} → (β → γ → MetaM α) → MetaM α) {α : Type} (k : β → γ → m α) : m α

Equations

• Lean.Meta.map2MetaM f k = controlAt Lean.MetaM fun (runInBase : {β : Type} → m β → Lean.MetaM (stM Lean.MetaM m β)) => f fun (b : β) (c : γ) => runInBase (k b c)

@[inline]

def Lean.Meta.map3MetaM {m : Type → Type u_1} {β : Sort u_2} {γ : Sort u_3} {δ : Sort u_4} [MonadControlT MetaM m] [Monad m] (f : {α : Type} → (β → γ → δ → MetaM α) → MetaM α) {α : Type} (k : β → γ → δ → m α) : m α

Equations

• Lean.Meta.map3MetaM f k = controlAt Lean.MetaM fun (runInBase : {β : Type} → m β → Lean.MetaM (stM Lean.MetaM m β)) => f fun (b : β) (c : γ) (d : δ) => runInBase (k b c d)

@[inline]

def Lean.Meta.modifyCache (f : Cache → Cache) : MetaM Unit

Equations

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

def Lean.Meta.resetCache : MetaM Unit

Equations

• Lean.Meta.resetCache = Lean.Meta.modifyCache fun (x : Lean.Meta.Cache) => { }

@[inline]

def Lean.Meta.modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit

Equations

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

@[inline]

def Lean.Meta.modifyDefEqTransientCache (f : DefEqCache → DefEqCache) : MetaM Unit

Equations

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

@[inline]

def Lean.Meta.modifyDefEqPermCache (f : DefEqCache → DefEqCache) : MetaM Unit

Equations

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

def Lean.Meta.mkExprConfigCacheKey (expr : Expr) : MetaM ExprConfigCacheKey

Equations

• Lean.Meta.mkExprConfigCacheKey expr = do let __do_lift ← read pure { expr := expr, configKey := __do_lift.configKey }

def Lean.Meta.mkDefEqCacheKey (lhs rhs : Expr) : MetaM DefEqCacheKey

Equations

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

def Lean.Meta.mkInfoCacheKey (expr : Expr) (nargs? : Option Nat) : MetaM InfoCacheKey

Equations

• Lean.Meta.mkInfoCacheKey expr nargs? = do let __do_lift ← read pure { configKey := __do_lift.configKey, expr := expr, nargs? := nargs? }

@[inline]

def Lean.Meta.resetDefEqPermCaches : MetaM Unit

Equations

• Lean.Meta.resetDefEqPermCaches = Lean.Meta.modifyDefEqPermCache fun (x : Lean.Meta.DefEqCache) => { }

@[inline]

def Lean.Meta.resetSynthInstanceCache : MetaM Unit

Equations

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

@[inline]

def Lean.Meta.modifyDiag (f : Diagnostics → Diagnostics) : MetaM Unit

Equations

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

def Lean.Meta.recordUnfold (declName : Name) : MetaM Unit

If diagnostics are enabled, record that declName has been unfolded.

Equations

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

def Lean.Meta.recordDefEqHeuristic (declName : Name) : MetaM Unit

If diagnostics are enabled, record that heuristic for solving f a =?= f b has been used.

Equations

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

def Lean.Meta.recordInstance (declName : Name) : MetaM Unit

If diagnostics are enabled, record that instance declName was used during TC resolution.

Equations

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

def Lean.Meta.recordSynthPendingFailure (type : Expr) : MetaM Unit

If diagnostics are enabled, record that synth pending failures.

Equations

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

def Lean.Meta.getLocalInstances : MetaM LocalInstances

Equations

• Lean.Meta.getLocalInstances = do let __do_lift ← read pure __do_lift.localInstances

def Lean.Meta.getConfig : MetaM Config

Equations

• Lean.Meta.getConfig = do let __do_lift ← read pure __do_lift.config

def Lean.Meta.getConfigWithKey : MetaM ConfigWithKey

Equations

• Lean.Meta.getConfigWithKey = do let __do_lift ← Lean.Meta.getConfig pure __do_lift.toConfigWithKey

def Lean.Meta.getPostponed : MetaM (PersistentArray PostponedEntry)

Return the array of postponed universe level constraints.

Equations

• Lean.Meta.getPostponed = do let __do_lift ← get pure __do_lift.postponed

def Lean.Meta.setPostponed (postponed : PersistentArray PostponedEntry) : MetaM Unit

Set the array of postponed universe level constraints.

Equations

• Lean.Meta.setPostponed postponed = modify fun (s : Lean.Meta.State) => { mctx := s.mctx, cache := s.cache, zetaDeltaFVarIds := s.zetaDeltaFVarIds, postponed := postponed, diag := s.diag }

@[inline]

def Lean.Meta.modifyPostponed (f : PersistentArray PostponedEntry → PersistentArray PostponedEntry) : MetaM Unit

Modify the array of postponed universe level constraints.

Equations

• Lean.Meta.modifyPostponed f = modify fun (s : Lean.Meta.State) => { mctx := s.mctx, cache := s.cache, zetaDeltaFVarIds := s.zetaDeltaFVarIds, postponed := f s.postponed, diag := s.diag }

def Lean.Meta.useEtaStruct (inductName : Name) : MetaM Bool

useEtaStruct inductName return true if we eta for structures is enabled for for the inductive datatype inductName.

Recall we have three different settings: .none (never use it), .all (always use it), .notClasses (enabled only for structure-like inductive types that are not classes).

The parameter inductName affects the result only if the current setting is .notClasses.

Equations

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

WARNING: The following 4 constants are a hack for simulating forward declarations. They are defined later using the export attribute. This is hackish because we have to hard-code the true arity of these definitions here, and make sure the C names match. We have used another hack based on IO.Refs in the past, it was safer but less efficient.

@[extern lean_whnf]

opaque Lean.Meta.whnf : Expr → MetaM Expr

Reduces an expression to its weak head normal form. This is when the "head" of the top-level expression has been fully reduced. The result may contain subexpressions that have not been reduced.

See Lean.Meta.whnfImp for the implementation.

@[extern lean_infer_type]

opaque Lean.Meta.inferType : Expr → MetaM Expr

Returns the inferred type of the given expression. Assumes the expression is type-correct.

The type inference algorithm does not do general type checking. Type inference only looks at subterms that are necessary for determining an expression's type, and as such if inferType succeeds it does not mean the term is type-correct. If an expression is sufficiently ill-formed that it prevents inferType from computing a type, then it will fail with a type error.

For typechecking during elaboration, see Lean.Meta.check. (Note that we do not guarantee that the elaborator typechecker is as correct or as efficient as the kernel typechecker. The kernel typechecker is invoked when a definition is added to the environment.)

Here are examples of type-incorrect terms for which inferType succeeds:

public import Lean

public section

open Lean Meta

/--
`@id.{1} Bool Nat.zero`.
In general, the type of `@id α x` is `α`.
-/
def e1 : Expr := mkApp2 (.const ``id [1]) (.const ``Bool []) (.const ``Nat.zero [])
#eval inferType e1
-- Lean.Expr.const `Bool []
#eval check e1
-- error: application type mismatch

/--
`let x : Int := Nat.zero; true`.
In general, the type of `let x := v; e`, if `e` does not reference `x`, is the type of `e`.
-/
def e2 : Expr := .letE `x (.const ``Int []) (.const ``Nat.zero []) (.const ``true []) false
#eval inferType e2
-- Lean.Expr.const `Bool []
#eval check e2
-- error: invalid let declaration

Here is an example of a type-incorrect term that makes inferType fail:

/--
`Nat.zero Nat.zero`
-/
def e3 : Expr := .app (.const ``Nat.zero []) (.const ``Nat.zero [])
#eval inferType e3
-- error: function expected

See Lean.Meta.inferTypeImp for the implementation of inferType.

@[extern lean_is_expr_def_eq]

opaque Lean.Meta.isExprDefEqAux : Expr → Expr → MetaM Bool

@[extern lean_is_level_def_eq]

opaque Lean.Meta.isLevelDefEqAux : Level → Level → MetaM Bool

@[extern lean_synth_pending]

opaque Lean.Meta.synthPending : MVarId → MetaM Bool

def Lean.Meta.whnfForall (e : Expr) : MetaM Expr

Equations

• Lean.Meta.whnfForall e = do let e' ← Lean.Meta.whnf e if e'.isForall = true then pure e' else pure e

def Lean.Meta.withIncRecDepth {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (x : n α) : n α

Equations

• Lean.Meta.withIncRecDepth x = Lean.Meta.mapMetaM (fun {α : Type} => Lean.withIncRecDepth) x

def Lean.Meta.mkFreshExprMVarAt (lctx : LocalContext) (localInsts : LocalInstances) (type : Expr) (kind : MetavarKind := MetavarKind.natural) (userName : Name := Name.anonymous) (numScopeArgs : Nat := 0) : MetaM Expr

Equations

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

def Lean.Meta.mkFreshLevelMVar : MetaM Level

Equations

• Lean.Meta.mkFreshLevelMVar = do let mvarId ← Lean.mkFreshLMVarId Lean.modifyMCtx fun (mctx : Lean.MetavarContext) => mctx.addLevelMVarDecl mvarId pure (Lean.mkLevelMVar mvarId)

def Lean.Meta.mkFreshExprMVar (type? : Option Expr) (kind : MetavarKind := MetavarKind.natural) (userName : Name := Name.anonymous) : MetaM Expr

Equations

• Lean.Meta.mkFreshExprMVar type? kind userName = Lean.Meta.mkFreshExprMVarImpl✝ type? kind userName

def Lean.Meta.mkFreshTypeMVar (kind : MetavarKind := MetavarKind.natural) (userName : Name := Name.anonymous) : MetaM Expr

Equations

• Lean.Meta.mkFreshTypeMVar kind userName = do let u ← Lean.Meta.mkFreshLevelMVar Lean.Meta.mkFreshExprMVar (some (Lean.mkSort u)) kind userName

def Lean.Meta.mkFreshExprMVarWithId (mvarId : MVarId) (type? : Option Expr := none) (kind : MetavarKind := MetavarKind.natural) (userName : Name := Name.anonymous) : MetaM Expr

Equations

• One or more equations did not get rendered due to their size.
• Lean.Meta.mkFreshExprMVarWithId mvarId (some type) kind userName = Lean.Meta.mkFreshExprMVarWithIdCore✝ mvarId type kind userName

def Lean.Meta.mkFreshLevelMVars (num : Nat) : MetaM (List Level)

Equations

• Lean.Meta.mkFreshLevelMVars num = num.foldM (fun (x : Nat) (x : x < num) (us : List Lean.Level) => do let __do_lift ← Lean.Meta.mkFreshLevelMVar pure (__do_lift :: us)) []

def Lean.Meta.mkFreshLevelMVarsFor (info : ConstantInfo) : MetaM (List Level)

Equations

• Lean.Meta.mkFreshLevelMVarsFor info = Lean.Meta.mkFreshLevelMVars info.numLevelParams

def Lean.Meta.mkConstWithFreshMVarLevels (declName : Name) : MetaM Expr

Create a constant with the given name and new universe metavariables. Example: mkConstWithFreshMVarLevels `Monad returns @Monad.{?u, ?v}

Equations

• Lean.Meta.mkConstWithFreshMVarLevels declName = do let info ← Lean.getConstInfo declName let __do_lift ← Lean.Meta.mkFreshLevelMVarsFor info pure (Lean.mkConst declName __do_lift)

def Lean.Meta.getTransparency : MetaM TransparencyMode

Return current transparency setting/mode.

Equations

• Lean.Meta.getTransparency = do let __do_lift ← Lean.Meta.getConfig pure __do_lift.transparency

def Lean.Meta.shouldReduceAll : MetaM Bool

Equations

• Lean.Meta.shouldReduceAll = do let __do_lift ← Lean.Meta.getTransparency pure (__do_lift == Lean.Meta.TransparencyMode.all)

def Lean.Meta.shouldReduceReducibleOnly : MetaM Bool

Equations

• Lean.Meta.shouldReduceReducibleOnly = do let __do_lift ← Lean.Meta.getTransparency pure (__do_lift == Lean.Meta.TransparencyMode.reducible)

def Lean.MVarId.findDecl? (mvarId : MVarId) : MetaM (Option MetavarDecl)

Return some mvarDecl where mvarDecl is mvarId declaration in the current metavariable context. Return none if mvarId has no declaration in the current metavariable context.

Equations

• mvarId.findDecl? = do let __do_lift ← Lean.getMCtx pure (__do_lift.findDecl? mvarId)

def Lean.MVarId.getDecl (mvarId : MVarId) : MetaM MetavarDecl

Return mvarId declaration in the current metavariable context. Throw an exception if mvarId is not declared in the current metavariable context.

Equations

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

def Lean.MVarId.getKind (mvarId : MVarId) : MetaM MetavarKind

Return mvarId kind. Throw an exception if mvarId is not declared in the current metavariable context.

Equations

• mvarId.getKind = do let __do_lift ← mvarId.getDecl pure __do_lift.kind

def Lean.Meta.isSyntheticMVar (e : Expr) : MetaM Bool

Return true if e is a synthetic (or synthetic opaque) metavariable

Equations

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

def Lean.MVarId.setKind (mvarId : MVarId) (kind : MetavarKind) : MetaM Unit

Set mvarId kind in the current metavariable context.

Equations

• mvarId.setKind kind = Lean.modifyMCtx fun (mctx : Lean.MetavarContext) => mctx.setMVarKind mvarId kind

def Lean.MVarId.setType (mvarId : MVarId) (type : Expr) : MetaM Unit

Update the type of the given metavariable. This function assumes the new type is definitionally equal to the current one

Equations

• mvarId.setType type = Lean.modifyMCtx fun (mctx : Lean.MetavarContext) => mctx.setMVarType mvarId type

def Lean.MVarId.isReadOnly (mvarId : MVarId) : MetaM Bool

Return true if the given metavariable is "read-only". That is, its depth is different from the current metavariable context depth.

Equations

• mvarId.isReadOnly = do let __do_lift ← mvarId.getDecl let __do_lift_1 ← Lean.getMCtx pure (__do_lift.depth != __do_lift_1.depth)

def Lean.MVarId.isReadOnlyOrSyntheticOpaque (mvarId : MVarId) : MetaM Bool

Returns true if mvarId.isReadOnly returns true or if mvarId is a synthetic opaque metavariable.

Recall isDefEq will not assign a value to mvarId if mvarId.isReadOnlyOrSyntheticOpaque.

Equations

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

def Lean.LMVarId.getLevel (mvarId : LMVarId) : MetaM Nat

Return the level of the given universe level metavariable.

Equations

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

def Lean.LMVarId.isReadOnly (mvarId : LMVarId) : MetaM Bool

Return true if the given universe metavariable is "read-only". That is, its depth is different from the current metavariable context depth.

Equations

• mvarId.isReadOnly = do let __do_lift ← mvarId.getLevel let __do_lift_1 ← Lean.getMCtx pure (decide (__do_lift < __do_lift_1.levelAssignDepth))

def Lean.MVarId.setUserName (mvarId : MVarId) (newUserName : Name) : MetaM Unit

Set the user-facing name for the given metavariable.

Equations

• mvarId.setUserName newUserName = Lean.modifyMCtx fun (mctx : Lean.MetavarContext) => mctx.setMVarUserName mvarId newUserName

def Lean.FVarId.throwUnknown {α : Type} (fvarId : FVarId) : CoreM α

Throw an exception saying fvarId is not declared in the current local context.

Equations

• fvarId.throwUnknown = Lean.throwError (Lean.toMessageData "unknown free variable `" ++ Lean.toMessageData (Lean.mkFVar fvarId) ++ Lean.toMessageData "`")

def Lean.FVarId.findDecl? (fvarId : FVarId) : MetaM (Option LocalDecl)

Return some decl if fvarId is declared in the current local context.

Equations

• fvarId.findDecl? = do let __do_lift ← Lean.getLCtx pure (__do_lift.find? fvarId)

def Lean.FVarId.getDecl (fvarId : FVarId) : MetaM LocalDecl

Return the local declaration for the given free variable. Throw an exception if local declaration is not in the current local context.

Equations

• fvarId.getDecl = do let __do_lift ← Lean.getLCtx match __do_lift.find? fvarId with | some d => pure d | none => liftM fvarId.throwUnknown

def Lean.FVarId.getType (fvarId : FVarId) : MetaM Expr

Return the type of the given free variable.

Equations

• fvarId.getType = do let __do_lift ← fvarId.getDecl pure __do_lift.type

def Lean.FVarId.getBinderInfo (fvarId : FVarId) : MetaM BinderInfo

Return the binder information for the given free variable.

Equations

• fvarId.getBinderInfo = do let __do_lift ← fvarId.getDecl pure __do_lift.binderInfo

def Lean.FVarId.getValue? (fvarId : FVarId) (allowNondep : Bool := false) : MetaM (Option Expr)

Returns some value if the given free let-variable has a visible local definition in the current local context (using Lean.LocalDecl.value?), and none otherwise.

Setting allowNondep := true allows access of the normally hidden value of a nondependent let declaration.

Equations

• fvarId.getValue? allowNondep = do let __do_lift ← fvarId.getDecl pure (__do_lift.value? allowNondep)

def Lean.FVarId.getUserName (fvarId : FVarId) : MetaM Name

Return the user-facing name for the given free variable.

Equations

• fvarId.getUserName = do let __do_lift ← fvarId.getDecl pure __do_lift.userName

def Lean.FVarId.isLetVar (fvarId : FVarId) (allowNondep : Bool := false) : MetaM Bool

Returns true if the free variable is a let-variable with a visible local definition in the current local context (using Lean.LocalDecl.isLet).

Setting allowNondep := true includes nondependent let declarations, whose values are normally hidden.

Equations

• fvarId.isLetVar allowNondep = do let __do_lift ← fvarId.getDecl pure (__do_lift.isLet allowNondep)

def Lean.Meta.getFVarLocalDecl (fvar : Expr) : MetaM LocalDecl

Get the local declaration associated to the given Expr in the current local context. Fails if the given expression is not a fvar or if no such declaration exists.

Equations

• Lean.Meta.getFVarLocalDecl fvar = fvar.fvarId!.getDecl

def Lean.FVarId.hasForwardDeps (fvarId : FVarId) : MetaM Bool

Returns true if another local declaration in the local context depends on fvarId.

Equations

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

def Lean.Meta.getLocalDeclFromUserName (userName : Name) : MetaM LocalDecl

Given a user-facing name for a free variable, return its declaration in the current local context. Throw an exception if free variable is not declared.

Equations

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

def Lean.Meta.getFVarFromUserName (userName : Name) : MetaM Expr

Given a user-facing name for a free variable, return the free variable or throw if not declared.

Equations

• Lean.Meta.getFVarFromUserName userName = do let d ← Lean.Meta.getLocalDeclFromUserName userName pure (Lean.Expr.fvar d.fvarId)

@[inline]

def Lean.Meta.liftMkBindingM {α : Type} (x : MetavarContext.MkBindingM α) : MetaM α

Lift a MkBindingM monadic action x to MetaM.

Equations

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

def Lean.Expr.abstractRangeM (e : Expr) (n : Nat) (xs : Array Expr) : MetaM Expr

Similar to abstractM but consider only the first min n xs.size entries in xs

It is also similar to Expr.abstractRange, but handles metavariables correctly. It uses elimMVarDeps to ensure e and the type of the free variables xs do not contain a metavariable ?m s.t. local context of ?m contains a free variable in xs.

Equations

• e.abstractRangeM n xs = Lean.Meta.liftMkBindingM (Lean.MetavarContext.abstractRange e n xs)

def Lean.Expr.abstractM (e : Expr) (xs : Array Expr) : MetaM Expr

Replace free (or meta) variables xs with loose bound variables. Similar to Expr.abstract, but handles metavariables correctly.

Equations

• e.abstractM xs = e.abstractRangeM xs.size xs

def Lean.Meta.collectForwardDeps (toRevert : Array Expr) (preserveOrder : Bool) (generalizeNondepLet : Bool := true) : MetaM (Array Expr)

Collect forward dependencies for the free variables in toRevert. Recall that when reverting free variables xs, we must also revert their forward dependencies.

When generalizeNondepLet := true (the default), then the values of nondependent lets are not considered when computing forward dependencies.

Equations

• Lean.Meta.collectForwardDeps toRevert preserveOrder generalizeNondepLet = Lean.Meta.liftMkBindingM (Lean.MetavarContext.collectForwardDeps toRevert preserveOrder generalizeNondepLet)

def Lean.Meta.mkForallFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly generalizeNondepLet : Bool := true) (binderInfoForMVars : BinderInfo := BinderInfo.implicit) : MetaM Expr

Takes an array xs of free variables or metavariables and a term e that may contain those variables, and abstracts and binds them as universal quantifiers.

• if usedOnly = true then only variables that the expression body depends on will appear.
• if usedLetOnly = true same as usedOnly except for let-bound variables. (That is, local constants which have been assigned a value.)
• if generalizeNondepLet = true then nondependent ldecls become foralls too.

Equations

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

def Lean.Meta.mkLambdaFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (etaReduce : Bool := false) (generalizeNondepLet : Bool := true) (binderInfoForMVars : BinderInfo := BinderInfo.implicit) : MetaM Expr

Takes an array xs of free variables and metavariables and a body term e and creates fun ..xs => e, suitably abstracting e and the types in xs.

Equations

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

def Lean.Meta.mkLetFVars (xs : Array Expr) (e : Expr) (usedLetOnly generalizeNondepLet : Bool := true) (binderInfoForMVars : BinderInfo := BinderInfo.implicit) : MetaM Expr

Equations

• Lean.Meta.mkLetFVars xs e usedLetOnly generalizeNondepLet binderInfoForMVars = Lean.Meta.mkLambdaFVars xs e false usedLetOnly false generalizeNondepLet binderInfoForMVars

def Lean.Meta.mkFunUnit (a : Expr) : MetaM Expr

fun _ : Unit => a

Equations

• Lean.Meta.mkFunUnit a = do let __do_lift ← liftM (Lean.mkFreshUserName `x) pure (Lean.mkLambda __do_lift Lean.BinderInfo.default (Lean.mkConst `Unit) a)

def Lean.Meta.elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) : MetaM Expr

Equations

• Lean.Meta.elimMVarDeps xs e preserveOrder = if xs.isEmpty = true then pure e else Lean.Meta.liftMkBindingM (Lean.MetavarContext.elimMVarDeps xs e preserveOrder)

@[inline]

def Lean.Meta.withConfig {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (f : Config → Config) : n α → n α

withConfig f x executes x using the updated configuration object obtained by applying f.

Equations

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

@[inline]

def Lean.Meta.withConfigWithKey {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (c : ConfigWithKey) : n α → n α

Equations

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

@[inline]

def Lean.Meta.withCanUnfoldPred {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (p : Config → ConstantInfo → CoreM Bool) : n α → n α

Equations

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

@[inline]

def Lean.Meta.withIncSynthPending {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} : n α → n α

Equations

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

@[inline]

def Lean.Meta.withInTypeClassResolution {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} : n α → n α

Equations

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

@[inline]

def Lean.Meta.withFreshCache {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} : n α → n α

Equations

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

def Lean.Meta.withZetaDeltaSet {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (s : FVarIdSet) : n α → n α

If s is nonempty, then withZetaDeltaSet s x executes x with zetaDeltaSet := s. The cache is temporarily reset while executing x.

If s is empty, then runs x without changing zetaDeltaSet or resetting the cache.

See also withTrackingZetaDeltaSet for tracking zeta-delta reductions.

Equations

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

def Lean.Meta.getZetaDeltaFVarIds : MetaM FVarIdSet

Gets the current zetaDeltaFVarIds set. If Context.trackZetaDelta is true, then whnf adds to this set those local definitions that are unfolded ("zeta-delta reduced") .

See withTrackingZetaDelta and withTrackingZetaDeltaSet.

Equations

• Lean.Meta.getZetaDeltaFVarIds = do let __do_lift ← get pure __do_lift.zetaDeltaFVarIds

def Lean.Meta.addZetaDeltaFVarId (fvarId : FVarId) : MetaM Unit

Inserts fvarId into the zetaDeltaFVarIds set.

Equations

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

@[inline]

def Lean.Meta.withTrackingZetaDelta {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} : n α → n α

withTrackingZetaDelta x executes x while tracking zeta-delta reductions performed by whnf. Furthermore, the zetaDeltaFVarIds set is temporarily cleared, and also the cache is temporarily reset so that reductions are accurately tracked.

Any zeta-delta reductions recorded while executing x will not persist when leaving withTrackingZetaDelta.

Equations

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

@[deprecated Lean.Meta.withTrackingZetaDelta (since := "2025-06-12")]

def Lean.Meta.resetZetaDeltaFVarIds : MetaM Unit

Equations

• Lean.Meta.resetZetaDeltaFVarIds = modify fun (s : Lean.Meta.State) => { mctx := s.mctx, cache := s.cache, postponed := s.postponed, diag := s.diag }

def Lean.Meta.withTrackingZetaDeltaSet {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (s : FVarIdSet) : n α → n α

withTrackingZetaDeltaSet s x executes x in a context where zetaDeltaFVarIds has been temporarily cleared.

• If s is nonempty, zeta-delta tracking is enabled and zetaDeltaSet := s. Furthermore, the cache is temporarily reset so that zeta-delta tracking is accurate.
• If s is empty, then zeta-delta tracking is disabled. The zetaDeltaSet is not modified, and the cache is not cleared.

Any zeta-delta reductions recorded while executing x will not persist when leaving withTrackingZetaDeltaSet.

See also withZetaDeltaSet, which does not interact with zeta-delta tracking.

Equations

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

@[inline]

def Lean.Meta.withoutProofIrrelevance {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (x : n α) : n α

Equations

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

@[inline]

def Lean.Meta.withTransparency {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (mode : TransparencyMode) : n α → n α

Equations

• Lean.Meta.withTransparency mode = Lean.Meta.mapMetaM fun {α : Type} => withReader fun (x : Lean.Meta.Context) => Lean.Meta.Context.setTransparency✝ x mode

@[inline]

def Lean.Meta.withDefault {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (x : n α) : n α

withDefault x executes x using the default transparency setting.

Equations

• Lean.Meta.withDefault x = Lean.Meta.withTransparency Lean.Meta.TransparencyMode.default x

@[inline]

def Lean.Meta.withReducible {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (x : n α) : n α

withReducible x executes x using the reducible transparency setting. In this setting only definitions tagged as [reducible] are unfolded.

Equations

• Lean.Meta.withReducible x = Lean.Meta.withTransparency Lean.Meta.TransparencyMode.reducible x

@[inline]

def Lean.Meta.withReducibleAndInstances {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (x : n α) : n α

withReducibleAndInstances x executes x using the .instances transparency setting. In this setting only definitions tagged as [reducible] or type class instances are unfolded.

Equations

• Lean.Meta.withReducibleAndInstances x = Lean.Meta.withTransparency Lean.Meta.TransparencyMode.instances x

@[inline]

def Lean.Meta.withAtLeastTransparency {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (mode : TransparencyMode) : n α → n α

Execute x ensuring the transparency setting is at least mode. Recall that .all > .default > .instances > .reducible.

Equations

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

@[inline]

def Lean.Meta.withAssignableSyntheticOpaque {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (x : n α) : n α

Execute x allowing isDefEq to assign synthetic opaque metavariables.

Equations

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

@[inline]

def Lean.Meta.savingCache {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} : n α → n α

Equations

• Lean.Meta.savingCache = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.savingCacheImpl✝

def Lean.Meta.getTheoremInfo (info : ConstantInfo) : MetaM (Option ConstantInfo)

Equations

• Lean.Meta.getTheoremInfo info = do let __do_lift ← Lean.Meta.shouldReduceAll if __do_lift = true then pure (some info) else pure none

def Lean.Meta.withNewLocalInstance {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (className : Name) (fvar : Expr) : n α → n α

Add entry { className := className, fvar := fvar } to localInstances, and then execute continuation k.

Equations

• Lean.Meta.withNewLocalInstance className fvar = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withNewLocalInstanceImp✝ className fvar

def Lean.Meta.isClass? (type : Expr) : MetaM (Option Name)

isClass? type return some ClsName if type is an instance of the class ClsName. Example:

#eval do
  let x ← mkAppM ``Inhabited #[mkConst ``Nat]
  IO.println (← isClass? x)
  -- (some Inhabited)

Equations

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

def Lean.Meta.withNewLocalInstances {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (fvars : Array Expr) (j : Nat) : n α → n α

Equations

• Lean.Meta.withNewLocalInstances fvars j = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withNewLocalInstancesImpAux✝ fvars j

def Lean.Meta.forallTelescope {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (type : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations : Bool := false) : n α

Given type of the form forall xs, A, execute k xs A. This combinator will declare local declarations, create free variables for them, execute k with updated local context, and make sure the cache is restored after executing k.

If cleanupAnnotations is true, we apply Expr.cleanupAnnotations to each type in the telescope.

Equations

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

def Lean.Meta.mapForallTelescope' (f : Expr → Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr

Given a monadic function f that takes a type and a term of that type and produces a new term, lifts this to the monadic function that opens a ∀ telescope, applies f to the body, and then builds the lambda telescope term for the new term.

Equations

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

def Lean.Meta.mapForallTelescope (f : Expr → MetaM Expr) (forallTerm : Expr) : MetaM Expr

Given a monadic function f that takes a term and produces a new term, lifts this to the monadic function that opens a ∀ telescope, applies f to the body, and then builds the lambda telescope term for the new term.

Equations

• Lean.Meta.mapForallTelescope f forallTerm = Lean.Meta.mapForallTelescope' (fun (x e : Lean.Expr) => f e) forallTerm

def Lean.Meta.forallTelescopeReducing {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (type : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations whnfType : Bool := false) : n α

Similar to forallTelescope, but given type of the form forall xs, A, it reduces A and continues building the telescope if it is a forall.

If cleanupAnnotations is true, we apply Expr.cleanupAnnotations to each type in the telescope.

If whnfType is true, we give k the whnf of the resulting type. This is a free operation.

Equations

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

def Lean.Meta.forallBoundedTelescope {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (type : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → n α) (cleanupAnnotations whnfType : Bool := false) : n α

Similar to forallTelescopeReducing, stops constructing the telescope when it reaches size maxFVars.

If cleanupAnnotations is true, we apply Expr.cleanupAnnotations to each type in the telescope.

If whnfType is true, we give k the whnf of the resulting type. This is a free operation unless maxFVars? == some 0, in which case it computes the whnf.

Equations

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

def Lean.Meta.lambdaLetTelescope {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations : Bool := false) (preserveNondepLet : Bool := true) : n α

Similar to lambdaTelescope but for lambda and let expressions.

• If cleanupAnnotations is true, we apply Expr.cleanupAnnotations to each type in the telescope.
• If preserveNondep is false, all haves are converted to lets.

See also mapLambdaLetTelescope for entering and rebuilding the telescope.

Equations

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

def Lean.Meta.lambdaTelescope {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations : Bool := false) : n α

Given e of the form fun ..xs => A, execute k xs A. This combinator will declare local declarations, create free variables for them, execute k with updated local context, and make sure the cache is restored after executing k.

If cleanupAnnotations is true, we apply Expr.cleanupAnnotations to each type in the telescope.

Equations

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

def Lean.Meta.lambdaBoundedTelescope {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (e : Expr) (maxFVars : Nat) (k : Array Expr → Expr → n α) (cleanupAnnotations : Bool := false) : n α

Given e of the form fun ..xs ..ys => A, execute k xs (fun ..ys => A) where xs.size ≤ maxFVars. This combinator will declare local declarations, create free variables for them, execute k with updated local context, and make sure the cache is restored after executing k.

If cleanupAnnotations is true, we apply Expr.cleanupAnnotations to each type in the telescope.

Equations

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

def Lean.Meta.letTelescope {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (e : Expr) (k : Array Expr → Expr → n α) (cleanupAnnotations : Bool := false) (preserveNondepLet : Bool := true) (nondepLetOnly : Bool := false) : n α

Given e of the form let x₁ := v₁; ...; let xₙ := vₙ; A, executes k xs A, where xs is an array of free variables for the binders. The lets can also be haves.

• If cleanupAnnotations is true, applies Expr.cleanupAnnotations to each type in the telescope.
• If preserveNondep is false, all haves are converted to lets.
• If nondepLetOnly is true, then only haves are consumed (it stops at the first dependent let).

See also mapLetTelescope for entering and rebuilding the telescope.

Equations

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

def Lean.Meta.letBoundedTelescope {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (e : Expr) (maxFVars? : Option Nat) (k : Array Expr → Expr → n α) (cleanupAnnotations : Bool := false) (preserveNondepLet : Bool := true) (nondepLetOnly : Bool := false) : n α

Like letTelescope, but limits the number of let/haves consumed to maxFVars?. If maxFVars? is none, then this is the same as letTelescope.

Equations

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

def Lean.Meta.mapLambdaLetTelescope {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] [MonadLiftT MetaM n] (e : Expr) (k : Array Expr → Expr → n Expr) (cleanupAnnotations : Bool := false) (preserveNondepLet usedLetOnly : Bool := true) : n Expr

Evaluates k from within a lambdaLetTelescope, then uses mkLetFVars to rebuild the telescope.

Equations

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

def Lean.Meta.mapLetTelescope {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] [MonadLiftT MetaM n] (e : Expr) (k : Array Expr → Expr → n Expr) (cleanupAnnotations : Bool := false) (preserveNondepLet : Bool := true) (nondepLetOnly : Bool := false) (usedLetOnly : Bool := true) : n Expr

Evaluates k from within a letTelescope, then uses mkLetFVars to rebuild the telescope.

Equations

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

def Lean.Meta.getParamNames (declName : Name) : MetaM (Array Name)

Return the parameter names for the given global declaration.

Equations

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

def Lean.Meta.forallMetaTelescope (e : Expr) (kind : MetavarKind := MetavarKind.natural) : MetaM (Array Expr × Array BinderInfo × Expr)

Given e of the form forall ..xs, A, this combinator will create a new metavariable for each x in xs and instantiate A with these. Returns a product containing

• the new metavariables
• the binder info for the xs
• the instantiated A

Equations

• Lean.Meta.forallMetaTelescope e kind = Lean.Meta.forallMetaTelescopeReducingAux✝ e false none kind

def Lean.Meta.forallMetaTelescopeReducing (e : Expr) (maxMVars? : Option Nat := none) (kind : MetavarKind := MetavarKind.natural) : MetaM (Array Expr × Array BinderInfo × Expr)

Similar to forallMetaTelescope, but if e = forall ..xs, A it will reduce A to construct further mvars.

Equations

• Lean.Meta.forallMetaTelescopeReducing e maxMVars? kind = Lean.Meta.forallMetaTelescopeReducingAux✝ e true maxMVars? kind

def Lean.Meta.forallMetaBoundedTelescope (e : Expr) (maxMVars : Nat) (kind : MetavarKind := MetavarKind.natural) : MetaM (Array Expr × Array BinderInfo × Expr)

Similar to forallMetaTelescopeReducing, stops constructing the telescope when it reaches size maxMVars.

Equations

• Lean.Meta.forallMetaBoundedTelescope e maxMVars kind = Lean.Meta.forallMetaTelescopeReducingAux✝ e true (some maxMVars) kind

def Lean.Meta.lambdaMetaTelescope (e : Expr) (maxMVars? : Option Nat := none) : MetaM (Array Expr × Array BinderInfo × Expr)

Similar to forallMetaTelescopeReducingAux but for lambda expressions.

Equations

• Lean.Meta.lambdaMetaTelescope e maxMVars? = Lean.Meta.lambdaMetaTelescope.process✝ maxMVars? #[] #[] 0 e

def Lean.Meta.withLocalDecl {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (name : Name) (bi : BinderInfo) (type : Expr) (k : Expr → n α) (kind : LocalDeclKind := LocalDeclKind.default) : n α

Create a free variable x with name, binderInfo and type, add it to the context and run in k. Then revert the context.

Equations

• Lean.Meta.withLocalDecl name bi type k kind = Lean.Meta.map1MetaM (fun {α : Type} (k : Lean.Expr → Lean.MetaM α) => Lean.Meta.withLocalDeclImp✝ name bi type k kind) k

def Lean.Meta.withLocalDeclD {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (name : Name) (type : Expr) (k : Expr → n α) : n α

Equations

• Lean.Meta.withLocalDeclD name type k = Lean.Meta.withLocalDecl name Lean.BinderInfo.default type k

def Lean.Meta.withLocalDeclNoLocalInstanceUpdate {α : Type} (name : Name) (bi : BinderInfo) (type : Expr) (x : Expr → MetaM α) : MetaM α

Similar to withLocalDecl, but it does not check whether the new variable is a local instance or not.

Equations

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

def Lean.Meta.withLocalDecls {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} [Inhabited α] (declInfos : Array (Name × BinderInfo × (Array Expr → n Expr))) (k : Array Expr → n α) : n α

Append an array of free variables xs to the local context and execute k xs. declInfos takes the form of an array consisting of:

• the name of the variable
• the binder info of the variable
• a type constructor for the variable, where the array consists of all of the free variables defined prior to this one. This is needed because the type of the variable may depend on prior variables.

See withLocalDeclsD and withLocalDeclsDND for simpler variants.

Equations

• Lean.Meta.withLocalDecls declInfos k = Lean.Meta.withLocalDecls.loop✝ declInfos k #[]

def Lean.Meta.withLocalDeclsD {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} [Inhabited α] (declInfos : Array (Name × (Array Expr → n Expr))) (k : Array Expr → n α) : n α

Variant of withLocalDecls using BinderInfo.default

Equations

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

def Lean.Meta.withLocalDeclsDND {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} [Inhabited α] (declInfos : Array (Name × Expr)) (k : Array Expr → n α) : n α

Simpler variant of withLocalDeclsD for bringing variables into scope whose types do not depend on each other.

Equations

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

def Lean.Meta.withAuxDecl {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (shortDeclName : Name) (type : Expr) (declName : Name) (k : Expr → n α) : n α

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

Equations

• Lean.Meta.withAuxDecl shortDeclName type declName k = Lean.Meta.map1MetaM (fun {α : Type} (k : Lean.Expr → Lean.MetaM α) => Lean.Meta.withAuxDeclImp✝ shortDeclName type declName k) k

def Lean.Meta.withNewBinderInfos {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (bs : Array (FVarId × BinderInfo)) (k : n α) : n α

Equations

• Lean.Meta.withNewBinderInfos bs k = Lean.Meta.mapMetaM (fun {α : Type} (k : Lean.MetaM α) => Lean.Meta.withNewBinderInfosImp✝ bs k) k

def Lean.Meta.withInstImplicitAsImplicit {α : Type} (xs : Array Expr) (k : MetaM α) : MetaM α

Execute k using a local context where any x in xs that is tagged as instance implicit is treated as a regular implicit.

Equations

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

def Lean.Meta.withLetDecl {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (name : Name) (type val : Expr) (k : Expr → n α) (nondep : Bool := false) (kind : LocalDeclKind := LocalDeclKind.default) : n α

Add the local declaration <name> : <type> := <val> to the local context and execute k x, where x is a new free variable corresponding to the let-declaration. After executing k x, the local context is restored.

Equations

• Lean.Meta.withLetDecl name type val k nondep kind = Lean.Meta.map1MetaM (fun {α : Type} (k : Lean.Expr → Lean.MetaM α) => Lean.Meta.withLetDeclImp✝ name type val k nondep kind) k

def Lean.Meta.mapLetDecl {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] [MonadLiftT MetaM n] (name : Name) (type val : Expr) (k : Expr → n Expr) (nondep : Bool := false) (kind : LocalDeclKind := LocalDeclKind.default) (usedLetOnly : Bool := true) : n Expr

Runs k x with the local declaration <name> : <type> := <val> added to the local context, where x is the new free variable. Afterwards, the result is wrapped in the given let/have expression (according to the value of nondep).

• If usedLetOnly := true (the default) then the the let/have is not created if the variable is unused.

Equations

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

def Lean.Meta.withLocalInstancesImp {α : Type} (decls : List LocalDecl) (k : MetaM α) : MetaM α

Equations

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

def Lean.Meta.withLocalInstances {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (decls : List LocalDecl) : n α → n α

Register any local instance in decls

Equations

• Lean.Meta.withLocalInstances decls = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withLocalInstancesImp decls

def Lean.Meta.withExistingLocalDecls {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (decls : List LocalDecl) : n α → n α

withExistingLocalDecls decls k, adds the given local declarations to the local context, and then executes k. This method assumes declarations in decls have valid FVarIds. After executing k, the local context is restored.

Remark: this method is used, for example, to implement the match-compiler. Each match-alternative comes with a local declarations (corresponding to pattern variables), and we use withExistingLocalDecls to add them to the local context before we process them.

Equations

• Lean.Meta.withExistingLocalDecls decls = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withExistingLocalDeclsImp✝ decls

def Lean.Meta.withReplaceFVarId {α : Type} (fvarId : FVarId) (e : Expr) : MetaM α → MetaM α

Removes fvarId from the local context, and replaces occurrences of it with e. It is the responsibility of the caller to ensure that e is well-typed in the context of any occurrence of fvarId.

Equations

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

def Lean.Meta.withNewMCtxDepth {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (k : n α) (allowLevelAssignments : Bool := false) : n α

withNewMCtxDepth k executes k with a higher metavariable context depth, where metavariables created outside the withNewMCtxDepth (with a lower depth) cannot be assigned. If allowLevelAssignments is set to true, then the level metavariable depth is not increased, and level metavariables from the outer scope can be assigned. (This is used by TC synthesis.)

Equations

• Lean.Meta.withNewMCtxDepth k allowLevelAssignments = Lean.Meta.mapMetaM (fun {α : Type} => Lean.Meta.withNewMCtxDepthImp✝ allowLevelAssignments) k

def Lean.Meta.withLCtx {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (lctx : LocalContext) (localInsts : LocalInstances) : n α → n α

withLCtx lctx localInsts k replaces the local context and local instances, and then executes k. The local context and instances are restored after executing k. This method assumes that the local instances in localInsts are in the local context lctx.

Equations

• Lean.Meta.withLCtx lctx localInsts = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withLocalContextImp✝ lctx localInsts

def Lean.Meta.withLCtx' {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (lctx : LocalContext) : n α → n α

Simpler version of withLCtx which just updates the local context. It is the responsibility of the caller ensure the local instances are also properly updated.

Equations

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

def Lean.Meta.withErasedFVars {n : Type → Type} [MonadControlT MetaM n] [Monad n] {α : Type} [MonadLCtx n] [MonadLiftT MetaM n] (fvarIds : Array FVarId) (k : n α) : n α

Runs k in a local environment with the fvarIds erased.

Equations

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

def Lean.Meta.withFreshUserNamesSinceIdx {n : Type → Type} [MonadControlT MetaM n] [Monad n] {α : Type} [MonadLCtx n] [MonadLiftT MetaM n] (idx : Nat) (k : n α) : n α

Ensures that the user names of all local declarations after index idx have a macro scope.

Equations

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

def Lean.MVarId.withContext {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (mvarId : MVarId) : n α → n α

Executes x using the given metavariable LocalContext and LocalInstances. The type class resolution cache is flushed when executing x if its LocalInstances are different from the current ones.

Equations

• mvarId.withContext = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withMVarContextImp✝ mvarId

def Lean.Meta.withMCtx {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} (mctx : MetavarContext) : n α → n α

withMCtx mctx k replaces the metavariable context and then executes k. The metavariable context is restored after executing k.

This method is used to implement the type class resolution procedure.

Equations

• Lean.Meta.withMCtx mctx = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withMCtxImp✝ mctx

def Lean.Meta.withoutModifyingMCtx {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} : n α → n α

withoutModifyingMCtx k executes k and then restores the metavariable context.

Equations

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

@[inline]

def Lean.Meta.approxDefEq {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} : n α → n α

Execute x using approximate unification: foApprox, ctxApprox and quasiPatternApprox.

Equations

• Lean.Meta.approxDefEq = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.approxDefEqImp✝

@[inline]

def Lean.Meta.fullApproxDefEq {n : Type → Type u_1} [MonadControlT MetaM n] [Monad n] {α : Type} : n α → n α

Similar to approxDefEq, but uses all available approximations. We don't use constApprox by default at approxDefEq because it often produces undesirable solution for monadic code. For example, suppose we have pure (x > 0) which has type ?m Prop. We also have the goal [Pure ?m]. Now, assume the expected type is IO Bool. Then, the unification constraint ?m Prop =?= IO Bool could be solved as ?m := fun _ => IO Bool using constApprox, but this spurious solution would generate a failure when we try to solve [Pure (fun _ => IO Bool)]

Equations

• Lean.Meta.fullApproxDefEq = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.fullApproxDefEqImp✝

def Lean.Meta.normalizeLevel (u : Level) : MetaM Level

Instantiate assigned universe metavariables in u, and then normalize it.

Equations

• Lean.Meta.normalizeLevel u = do let u ← Lean.instantiateLevelMVars u pure u.normalize

def Lean.Meta.whnfR (e : Expr) : MetaM Expr

whnf with reducible transparency.

Equations

• Lean.Meta.whnfR e = Lean.Meta.withTransparency Lean.Meta.TransparencyMode.reducible (Lean.Meta.whnf e)

def Lean.Meta.whnfD (e : Expr) : MetaM Expr

whnf with default transparency.

Equations

• Lean.Meta.whnfD e = Lean.Meta.withTransparency Lean.Meta.TransparencyMode.default (Lean.Meta.whnf e)

def Lean.Meta.whnfI (e : Expr) : MetaM Expr

whnf with instances transparency.

Equations

• Lean.Meta.whnfI e = Lean.Meta.withTransparency Lean.Meta.TransparencyMode.instances (Lean.Meta.whnf e)

def Lean.Meta.whnfAtMostI (e : Expr) : MetaM Expr

whnf with at most instances transparency.

Equations

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

def Lean.Meta.setInlineAttribute (declName : Name) (kind : Compiler.InlineAttributeKind := Compiler.InlineAttributeKind.inline) : MetaM Unit

Mark declaration declName with the attribute [inline]. This method does not check whether the given declaration is a definition.

Recall that this attribute can only be set in the same module where declName has been declared.

Equations

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

def Lean.Meta.instantiateForall (e : Expr) (ps : Array Expr) : MetaM Expr

Given e of the form forall (a_1 : A_1) ... (a_n : A_n), B[a_1, ..., a_n] and p_1 : A_1, ... p_n : A_n, return B[p_1, ..., p_n].

Equations

• Lean.Meta.instantiateForall e ps = Lean.Meta.instantiateForallAux✝ ps 0 e

def Lean.Meta.instantiateLambda (e : Expr) (ps : Array Expr) : MetaM Expr

Given e of the form fun (a_1 : A_1) ... (a_n : A_n) => t[a_1, ..., a_n] and p_1 : A_1, ... p_n : A_n, return t[p_1, ..., p_n]. It uses whnf to reduce e if it is not a lambda

Equations

• Lean.Meta.instantiateLambda e ps = Lean.Meta.instantiateLambdaAux✝ ps 0 e

structure Lean.Meta.ExprParamInfo : Type

A simpler version of ParamInfo for information about the parameter of a forall or lambda.

• name : Name

  The name of the parameter.

• type : Expr

  The type of the parameter.

• binderInfo : BinderInfo

  The binder annotation for the parameter.

def Lean.Meta.instInhabitedExprParamInfo.default : ExprParamInfo

Equations

• Lean.Meta.instInhabitedExprParamInfo.default = { name := default, type := default, binderInfo := default }

instance Lean.Meta.instInhabitedExprParamInfo : Inhabited ExprParamInfo

Equations

• Lean.Meta.instInhabitedExprParamInfo = { default := Lean.Meta.instInhabitedExprParamInfo.default }

def Lean.Meta.instantiateForallWithParamInfos (e : Expr) (args : Array Expr) (cleanupAnnotations : Bool := false) : MetaM (Array ExprParamInfo × Expr)

Given e of the form ∀ (p₁ : P₁) … (p₁ : P₁), B[p_1,…,p_n] and arg₁ : P₁, …, argₙ : Pₙ, returns

• the names p₁, …, pₙ,
• the binder infos,
• the binder types P₁, P₂[arg₁], …, P[arg₁,…,argₙ₋₁], and
• the type B[arg₁,…,argₙ].

It uses whnf to reduce e if it is not a forall.

See also Lean.Meta.instantiateForall.

Equations

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

def Lean.Meta.instantiateLambdaWithParamInfos (e : Expr) (args : Array Expr) (cleanupAnnotations : Bool := false) : MetaM (Array ExprParamInfo × Expr)

Given e of the form fun (p₁ : P₁) … (p₁ : P₁) => t[p_1,…,p_n] and arg₁ : P₁, …, argₙ : Pₙ, returns

• the names p₁, …, pₙ,
• the binder infos,
• the binder types P₁, P₂[arg₁], …, P[arg₁,…,argₙ₋₁], and
• the term t[arg₁,…,argₙ].

It uses whnf to reduce e if it is not a lambda.

See also Lean.Meta.instantiateLambda.

Equations

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

def Lean.Meta.ppExprWithInfos (e : Expr) : MetaM FormatWithInfos

Pretty-print the given expression.

Equations

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

def Lean.Meta.ppExpr (e : Expr) : MetaM Format

Pretty-print the given expression.

Equations

• Lean.Meta.ppExpr e = (fun (x : Lean.FormatWithInfos) => x.fmt) <$> Lean.Meta.ppExprWithInfos e

@[inline]

def Lean.Meta.orElse {α : Type} (x : MetaM α) (y : Unit → MetaM α) : MetaM α

Equations

• Lean.Meta.orElse x y = do let s ← Lean.saveState tryCatch x fun (x : Lean.Exception) => do s.restore y ()

instance Lean.Meta.instOrElseMetaM {α : Type} : OrElse (MetaM α)

Equations

• Lean.Meta.instOrElseMetaM = { orElse := Lean.Meta.orElse }

instance Lean.Meta.instAlternativeMetaM : Alternative MetaM

Equations

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

@[inline]

def Lean.Meta.orelseMergeErrors {m : Type → Type u_1} {α : Type} [MonadControlT MetaM m] [Monad m] (x y : m α) (mergeRef : Syntax → Syntax → Syntax := fun (r₁ x : Syntax) => r₁) (mergeMsg : MessageData → MessageData → MessageData := fun (m₁ m₂ : MessageData) => m₁ ++ MessageData.ofFormat Format.line ++ MessageData.ofFormat Format.line ++ m₂) : m α

Similar to orelse, but merge errors. Note that internal errors are not caught. The default mergeRef uses the ref (position information) for the first message. The default mergeMsg combines error messages using Format.line ++ Format.line as a separator.

Equations

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

def Lean.Meta.mapErrorImp {α : Type} (x : MetaM α) (f : MessageData → MessageData) : MetaM α

Equations

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

@[inline]

def Lean.Meta.mapError {m : Type → Type u_1} {α : Type} [MonadControlT MetaM m] [Monad m] (x : m α) (f : MessageData → MessageData) : m α

Execute x, and apply f to the produced error message

Equations

• Lean.Meta.mapError x f = controlAt Lean.MetaM fun (runInBase : {β : Type} → m β → Lean.MetaM (stM Lean.MetaM m β)) => Lean.Meta.mapErrorImp (runInBase x) f

@[inline]

def Lean.Meta.prependError {m : Type → Type u_1} {α : Type} [MonadControlT MetaM m] [Monad m] (msg : MessageData) (x : m α) : m α

Execute x. If it throws an error, indent and prepend msg to it.

Equations

• Lean.Meta.prependError msg x = Lean.Meta.mapError x fun (e : Lean.MessageData) => Lean.toMessageData msg ++ Lean.toMessageData (Lean.indentD e)

def Lean.Meta.sortFVarIds (fvarIds : Array FVarId) : MetaM (Array FVarId)

Sort free variables using an order x < y iff x was defined before y. If a free variable is not in the local context, we use their id.

Equations

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

def Lean.Meta.isInductivePredicateVal (indVal : InductiveVal) : MetaM Bool

Return true if indVal is an inductive predicate. That is, inductive type in Prop.

Equations

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

def Lean.Meta.isInductivePredicate? (declName : Name) : MetaM (Option InductiveVal)

Return some info if declName is an inductive predicate where info : InductiveVal. That is, inductive type in Prop.

Equations

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

def Lean.Meta.isInductivePredicate (declName : Name) : MetaM Bool

Return true if declName is an inductive predicate. That is, inductive type in Prop.

Equations

• Lean.Meta.isInductivePredicate declName = do let __do_lift ← Lean.Meta.isInductivePredicate? declName pure __do_lift.isSome

def Lean.Meta.isListLevelDefEqAux : List Level → List Level → MetaM Bool

Equations

• Lean.Meta.isListLevelDefEqAux [] [] = pure true
• Lean.Meta.isListLevelDefEqAux (u :: us) (v :: vs) = (Lean.Meta.isLevelDefEqAux u v <&&> Lean.Meta.isListLevelDefEqAux us vs)
• Lean.Meta.isListLevelDefEqAux x✝¹ x✝ = pure false

def Lean.Meta.getNumPostponed : MetaM Nat

Equations

• Lean.Meta.getNumPostponed = do let __do_lift ← Lean.Meta.getPostponed pure __do_lift.size

def Lean.Meta.getResetPostponed : MetaM (PersistentArray PostponedEntry)

Equations

• Lean.Meta.getResetPostponed = do let ps ← Lean.Meta.getPostponed Lean.Meta.setPostponed { } pure ps

def Lean.Meta.mkLevelStuckErrorMessage (entry : PostponedEntry) : MetaM MessageData

Equations

• Lean.Meta.mkLevelStuckErrorMessage entry = Lean.Meta.mkLevelErrorMessageCore✝ "stuck at solving universe constraint" entry

def Lean.Meta.mkLevelErrorMessage (entry : PostponedEntry) : MetaM MessageData

Equations

• Lean.Meta.mkLevelErrorMessage entry = Lean.Meta.mkLevelErrorMessageCore✝ "failed to solve universe constraint" entry

def Lean.Meta.processPostponed (mayPostpone : Bool := true) (exceptionOnFailure : Bool := false) : MetaM Bool

Equations

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

@[specialize #[]]

def Lean.Meta.checkpointDefEq (x : MetaM Bool) (mayPostpone : Bool := true) : MetaM Bool

checkpointDefEq x executes x and process all postponed universe level constraints produced by x. We keep the modifications only if processPostponed return true and x returned true.

If mayPostpone == false, all new postponed universe level constraints must be solved before returning. We currently try to postpone universe constraints as much as possible, even when by postponing them we are not sure whether x really succeeded or not.

Equations

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

def Lean.Meta.isLevelDefEq (u v : Level) : MetaM Bool

Determines whether two universe level expressions are definitionally equal to each other.

Equations

• Lean.Meta.isLevelDefEq u v = Lean.Meta.checkpointDefEq (Lean.Meta.isLevelDefEqAux u v)

def Lean.Meta.isExprDefEq (t s : Expr) : MetaM Bool

See isDefEq.

Equations

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

@[reducible, inline]

abbrev Lean.Meta.isDefEq (t s : Expr) : MetaM Bool

Determines whether two expressions are definitionally equal to each other.

To control how metavariables are assigned and unified, metavariables and their context have a "depth". Given a metavariable ?m and a MetavarContext mctx, ?m is not assigned if ?m.depth != mctx.depth. The combinator withNewMCtxDepth x will bump the depth while executing x. So, withNewMCtxDepth (isDefEq a b) is isDefEq without any mvar assignment happening whereas isDefEq a b will assign any metavariables of the current depth in a and b to unify them.

For matching (where only mvars in b should be assigned), we create the term inside the withNewMCtxDepth. For an example, see Lean.Meta.Simp.tryTheoremWithExtraArgs?

Equations

• Lean.Meta.isDefEq t s = Lean.Meta.isExprDefEq t s

def Lean.Meta.isExprDefEqGuarded (a b : Expr) : MetaM Bool

Equations

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

@[reducible, inline]

abbrev Lean.Meta.isDefEqGuarded (t s : Expr) : MetaM Bool

Similar to isDefEq, but returns false if an exception has been thrown.

Equations

• Lean.Meta.isDefEqGuarded t s = Lean.Meta.isExprDefEqGuarded t s

def Lean.Meta.isDefEqNoConstantApprox (t s : Expr) : MetaM Bool

Equations

• Lean.Meta.isDefEqNoConstantApprox t s = Lean.Meta.approxDefEq (Lean.Meta.isDefEq t s)

@[extern lean_checked_assign]

opaque Lean.MVarId.checkedAssign (mvarId : MVarId) (val : Expr) : MetaM Bool

Returns true if mvarId := val was successfully assigned. This method uses the same assignment validation performed by isDefEq, but it does not check whether the types match.

def Lean.Meta.etaExpand (e : Expr) : MetaM Expr

Eta expand the given expression. Example:

etaExpand (mkConst ``Nat.add)

produces fun x y => Nat.add x y

Equations

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

def Lean.Meta.instantiateMVarsIfMVarApp (e : Expr) : MetaM Expr

If e is of the form ?m ... instantiate metavars

Equations

• Lean.Meta.instantiateMVarsIfMVarApp e = if e.getAppFn.isMVar = true then Lean.instantiateMVars e else pure e

def Lean.Meta.instantiateMVarsProfiling (e : Expr) : MetaM Expr

Equations

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

def Lean.Meta.realizeValue {α : Type u_1} {β : Type} [BEq α] [Hashable α] [TypeName α] [TypeName β] (forConst : Name) (key : α) (realize : MetaM β) : MetaM β

Realizes and caches a value for a given key with all environment objects derived from calling enableRealizationsForConst forConst (fails if not called yet). If this is the first environment branch passing the specific key, realize is called with the environment and options at the time of calling enableRealizationsForConst if forConst is from the current module and the state just after importing otherwise, thus helping achieve deterministic results despite the non-deterministic choice of which thread is tasked with realization. In other words, the result of realizeValue is as if realize had been called immediately after enableRealizationsForConst forConst, with most effects but the return value discarded (see below). Whether two calls of realizeValue with different forConsts but the same key share the result is undefined; in practice, the key should usually uniquely determine forConst by e.g. including it as a field.

realizeValue cannot check what other data is captured in the realize closure, so it is best practice to extract it into a separate function and pass only arguments uniquely determined by key. Traces, diagnostics, and raw std stream output of realize are reported at all callers via Core.logSnapshotTask (so that the location of generated diagnostics is deterministic). Note that, as realize is run using the options at declaration time of forConst, trace options must be set prior to that (or, for imported constants, on the cmdline) in order to be active. If realize throws an exception, it is rethrown at all callers.

Equations

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

def Lean.Meta.realizeConst (forConst constName : Name) (realize : MetaM Unit) : MetaM Unit

Makes the helper constant constName that is derived from forConst available in the environment. enableRealizationsForConst forConst must have been called first on this environment branch. If this is the first environment branch requesting constName to be realized (atomically), realize is called with the environment and options at the time of calling enableRealizationsForConst if forConst is from the current module and the state just after importing otherwise, thus helping achieve deterministic results despite the non-deterministic choice of which thread is tasked with realization. In other words, the state after calling realizeConst is as if realize had been called immediately after enableRealizationsForConst forConst, though the effects of this call are visible only after calling realizeConst. See below for more details on the replayed effects.

realizeConst cannot check what other data is captured in the realize closure, so it is best practice to extract it into a separate function and pay close attention to the passed arguments, if any. realize must return with constName added to the environment, at which point all callers of realizeConst with this constName will be unblocked and have access to an updated version of their own environment containing any new constants realize added, including recursively realized constants. Traces, diagnostics, and raw std stream output are reported at all callers via Core.logSnapshotTask (so that the location of generated diagnostics is deterministic). Note that, as realize is run using the options at declaration time of forConst, trace options must be set prior to that (or, for imported constants, on the cmdline) in order to be active. The environment extension state at the end of realize is available to each caller via EnvExtension.getState (asyncDecl := constName). If realize throws an exception or fails to add constName to the environment, an appropriate diagnostic is reported to all callers but no constants are added to the environment.

Equations

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

def Lean.PPContext.runCoreM {α : Type} (ppCtx : PPContext) (x : CoreM α) : IO α

Equations

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

def Lean.PPContext.runMetaM {α : Type} (ppCtx : PPContext) (x : MetaM α) : IO α

Equations

• ppCtx.runMetaM x = ppCtx.runCoreM (x.run' { lctx := ppCtx.lctx } { mctx := ppCtx.mctx })

def Lean.MessageData.ofLazyM (f : MetaM MessageData) (es : Array Expr := #[]) : MessageData

Turns a MetaM MessageData into a MessageData.lazy which will run the monadic value. The optional array of expressions is used to set the hasSyntheticSorry fields, and should comprise the expressions that are included in the message data.

Equations

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