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 : Lean.InternalExceptionId

structure Lean.Meta.Config : Type

• 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 exeption Exeption.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 solveable later after it assigns ?m.

• transparency : Lean.Meta.TransparencyMode

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

• zetaNonDep : Bool

  If zetaNonDep == false, then non dependent let-decls are not zeta expanded.

• trackZeta : Bool

  When trackZeta == true, we store zetaFVarIds all free variables that have been zeta-expanded.

• 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

• etaStruct : Lean.Meta.EtaStructMode

  Eta for structures configuration mode.

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

structure Lean.Meta.ParamInfo : Type

• binderInfo : Lean.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 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]

Function parameter information cache.

instance Lean.Meta.instInhabitedParamInfo : Inhabited Lean.Meta.ParamInfo

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

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

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

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

structure Lean.Meta.FunInfo : Type

• paramInfo : Array Lean.Meta.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.

Function information cache. See ParamInfo.

structure Lean.Meta.InfoCacheKey : Type

• transparency : Lean.Meta.TransparencyMode

  The transparency mode used to compute the FunInfo.

• expr : Lean.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 unsing the current transparency setting. X

Key for the function information cache.

instance Lean.Meta.instInhabitedInfoCacheKey : Inhabited Lean.Meta.InfoCacheKey

instance Lean.Meta.instBEqInfoCacheKey : BEq Lean.Meta.InfoCacheKey

instance Lean.Meta.InfoCacheKey.instHashableInfoCacheKey : Hashable Lean.Meta.InfoCacheKey

@[inline, reducible]

abbrev Lean.Meta.SynthInstanceCache : Type

@[inline, reducible]

abbrev Lean.Meta.InferTypeCache : Type

@[inline, reducible]

abbrev Lean.Meta.FunInfoCache : Type

@[inline, reducible]

abbrev Lean.Meta.WhnfCache : Type

@[inline, reducible]

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.

structure Lean.Meta.Cache : Type

• inferType : Lean.Meta.InferTypeCache
• funInfo : Lean.Meta.FunInfoCache
• synthInstance : Lean.Meta.SynthInstanceCache
• whnfDefault : Lean.Meta.WhnfCache
• whnfAll : Lean.Meta.WhnfCache
• defEq : Lean.Meta.DefEqCache

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

instance Lean.Meta.instInhabitedCache : Inhabited Lean.Meta.Cache

structure Lean.Meta.DefEqContext : Type

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

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

structure Lean.Meta.PostponedEntry : Type

• ref : Lean.Syntax

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

• lhs : Lean.Level
• rhs : Lean.Level
• ctx? : Option Lean.Meta.DefEqContext

  Context for the surrounding isDefEq call when entry was created.

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.

instance Lean.Meta.instInhabitedPostponedEntry : Inhabited Lean.Meta.PostponedEntry

structure Lean.Meta.State : Type

• mctx : Lean.MetavarContext
• cache : Lean.Meta.Cache
• zetaFVarIds : Lean.FVarIdSet

  When trackZeta == true, then any let-decl free variable that is zeta expansion performed by MetaM is stored in zetaFVarIds.

• postponed : Lean.PersistentArray Lean.Meta.PostponedEntry

  Array of postponed universe level constraints

MetaM monad state.

instance Lean.Meta.instInhabitedState : Inhabited Lean.Meta.State

structure Lean.Meta.SavedState : Type

• core : Lean.Core.State
• meta : Lean.Meta.State

Backtrackable state for the MetaM monad.

instance Lean.Meta.instNonemptySavedState : Nonempty Lean.Meta.SavedState

structure Lean.Meta.Context : Type

• config : Lean.Meta.Config
• lctx : Lean.LocalContext

  Local context

• localInstances : Lean.LocalInstances

  Local instances in lctx.

• defEqCtx? : Option Lean.Meta.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: in the current implementation, synthPending fails if synthPendingDepth > 0. We will add a configuration option if necessary.

• canUnfold? : Option (Lean.Meta.Config → Lean.ConstantInfo → Lean.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.

Contextual information for the MetaM monad.

@[inline, reducible]

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

@[always_inline]

instance Lean.Meta.instMonadMetaM : Monad Lean.MetaM

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

instance Lean.Meta.instMonadLCtxMetaM : Lean.MonadLCtx Lean.MetaM

instance Lean.Meta.instMonadMCtxMetaM : Lean.MonadMCtx Lean.MetaM

instance Lean.Meta.instMonadEnvMetaM : Lean.MonadEnv Lean.MetaM

instance Lean.Meta.instAddMessageContextMetaM : Lean.AddMessageContext Lean.MetaM

def Lean.Meta.saveState : Lean.MetaM Lean.Meta.SavedState

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

Restore backtrackable parts of the state.

instance Lean.Meta.instMonadBacktrackSavedStateMetaM : Lean.MonadBacktrack Lean.Meta.SavedState Lean.MetaM

@[inline]

def Lean.Meta.MetaM.run {α : Type} (x : Lean.MetaM α) (ctx : optParam Lean.Meta.Context { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, transparency := Lean.Meta.TransparencyMode.default, zetaNonDep := true, trackZeta := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true, etaStruct := Lean.Meta.EtaStructMode.all }, lctx := { fvarIdToDecl := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none }) (s : optParam Lean.Meta.State { mctx := { depth := 0, levelAssignDepth := 0, mvarCounter := 0, lDepth := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, cache := { inferType := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, funInfo := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, synthInstance := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfDefault := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfAll := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEq := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, zetaFVarIds := ∅, postponed := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }) : Lean.CoreM (α × Lean.Meta.State)

@[inline]

def Lean.Meta.MetaM.run' {α : Type} (x : Lean.MetaM α) (ctx : optParam Lean.Meta.Context { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, transparency := Lean.Meta.TransparencyMode.default, zetaNonDep := true, trackZeta := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true, etaStruct := Lean.Meta.EtaStructMode.all }, lctx := { fvarIdToDecl := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none }) (s : optParam Lean.Meta.State { mctx := { depth := 0, levelAssignDepth := 0, mvarCounter := 0, lDepth := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, cache := { inferType := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, funInfo := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, synthInstance := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfDefault := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfAll := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEq := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, zetaFVarIds := ∅, postponed := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }) : Lean.CoreM α

@[inline]

def Lean.Meta.MetaM.toIO {α : Type} (x : Lean.MetaM α) (ctxCore : Lean.Core.Context) (sCore : Lean.Core.State) (ctx : optParam Lean.Meta.Context { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, transparency := Lean.Meta.TransparencyMode.default, zetaNonDep := true, trackZeta := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true, etaStruct := Lean.Meta.EtaStructMode.all }, lctx := { fvarIdToDecl := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none }) (s : optParam Lean.Meta.State { mctx := { depth := 0, levelAssignDepth := 0, mvarCounter := 0, lDepth := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, cache := { inferType := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, funInfo := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, synthInstance := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfDefault := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfAll := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEq := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, zetaFVarIds := ∅, postponed := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }) : IO (α × Lean.Core.State × Lean.Meta.State)

instance Lean.Meta.instMetaEvalMetaM {α : Type} [Lean.MetaEval α] : Lean.MetaEval (Lean.MetaM α)

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

def Lean.Meta.getLocalInstances : Lean.MetaM Lean.LocalInstances

def Lean.Meta.getConfig : Lean.MetaM Lean.Meta.Config

def Lean.Meta.resetZetaFVarIds : Lean.MetaM Unit

def Lean.Meta.getZetaFVarIds : Lean.MetaM Lean.FVarIdSet

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

Return the array of postponed universe level constraints.

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

Set the array of postponed universe level constraints.

@[inline]

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

Modify the array of postponed universe level constraints.

def Lean.Meta.useEtaStruct (inductName : Lake.Name) : Lean.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.

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 6 lean_whnf]

opaque Lean.Meta.whnf : Lean.Expr → Lean.MetaM Lean.Expr

Reduces an expression to its Weak Head Normal Form. This is when the topmost expression has been fully reduced, but may contain subexpressions which have not been reduced.

@[extern 6 lean_infer_type]

opaque Lean.Meta.inferType : Lean.Expr → Lean.MetaM Lean.Expr

Returns the inferred type of the given expression, or fails if it is not type-correct.

@[extern 7 lean_is_expr_def_eq]

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

@[extern 7 lean_is_level_def_eq]

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

@[extern 6 lean_synth_pending]

opaque Lean.Meta.synthPending : Lean.MVarId → Lean.MetaM Bool

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

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

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

def Lean.Meta.mkFreshLevelMVar : Lean.MetaM Lean.Level

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

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

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

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

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

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

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

def Lean.Meta.getTransparency : Lean.MetaM Lean.Meta.TransparencyMode

Return current transparency setting/mode.

def Lean.Meta.shouldReduceAll : Lean.MetaM Bool

def Lean.Meta.shouldReduceReducibleOnly : Lean.MetaM Bool

def Lean.MVarId.findDecl? (mvarId : Lean.MVarId) : Lean.MetaM (Option Lean.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.

@[deprecated Lean.MVarId.findDecl?]

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

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

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

@[deprecated Lean.MVarId.getDecl]

def Lean.Meta.getMVarDecl (mvarId : Lean.MVarId) : Lean.MetaM Lean.MetavarDecl

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

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

@[deprecated Lean.MVarId.getKind]

def Lean.Meta.getMVarDeclKind (mvarId : Lean.MVarId) : Lean.MetaM Lean.MetavarKind

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

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

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

Set mvarId kind in the current metavariable context.

@[deprecated Lean.MVarId.setKind]

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

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

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

@[deprecated Lean.MVarId.setType]

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

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

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

@[deprecated Lean.MVarId.isReadOnly]

def Lean.Meta.isReadOnlyExprMVar (mvarId : Lean.MVarId) : Lean.MetaM Bool

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

Return true if mvarId.isReadOnly return true or if mvarId is a synthetic opaque metavariable.

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

@[deprecated Lean.MVarId.isReadOnlyOrSyntheticOpaque]

def Lean.Meta.isReadOnlyOrSyntheticOpaqueExprMVar (mvarId : Lean.MVarId) : Lean.MetaM Bool

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

Return the level of the given universe level metavariable.

@[deprecated Lean.LMVarId.getLevel]

def Lean.Meta.getLevelMVarDepth (mvarId : Lean.LMVarId) : Lean.MetaM Nat

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

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

@[deprecated Lean.LMVarId.isReadOnly]

def Lean.Meta.isReadOnlyLevelMVar (mvarId : Lean.LMVarId) : Lean.MetaM Bool

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

Set the user-facing name for the given metavariable.

@[deprecated Lean.MVarId.setUserName]

def Lean.Meta.setMVarUserName (mvarId : Lean.MVarId) (userNameNew : Lake.Name) : Lean.MetaM Unit

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

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

@[deprecated Lean.FVarId.throwUnknown]

def Lean.Meta.throwUnknownFVar {α : Type} (fvarId : Lean.FVarId) : Lean.MetaM α

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

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

@[deprecated Lean.FVarId.findDecl?]

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

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

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

@[deprecated Lean.FVarId.getDecl]

def Lean.Meta.getLocalDecl (fvarId : Lean.FVarId) : Lean.MetaM Lean.LocalDecl

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

Return the type of the given free variable.

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

Return the binder information for the given free variable.

def Lean.FVarId.getValue? (fvarId : Lean.FVarId) : Lean.MetaM (Option Lean.Expr)

Return some value if the given free variable is a let-declaration, and none otherwise.

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

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

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

Return true is the free variable is a let-variable.

def Lean.Meta.getFVarLocalDecl (fvar : Lean.Expr) : Lean.MetaM Lean.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.

def Lean.Meta.getLocalDeclFromUserName (userName : Lake.Name) : Lean.MetaM Lean.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.

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

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

@[inline]

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

Lift a MkBindingM monadic action x to MetaM.

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

Similar to abstracM 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.

@[deprecated Lean.Expr.abstractRangeM]

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

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

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

@[deprecated Lean.Expr.abstractM]

def Lean.Meta.abstract (e : Lean.Expr) (xs : Array Lean.Expr) : Lean.MetaM Lean.Expr

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

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

def Lean.Meta.mkForallFVars (xs : Array Lean.Expr) (e : Lean.Expr) (usedOnly : optParam Bool false) (usedLetOnly : optParam Bool true) (binderInfoForMVars : optParam Lean.BinderInfo Lean.BinderInfo.implicit) : Lean.MetaM Lean.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.)

def Lean.Meta.mkLambdaFVars (xs : Array Lean.Expr) (e : Lean.Expr) (usedOnly : optParam Bool false) (usedLetOnly : optParam Bool true) (binderInfoForMVars : optParam Lean.BinderInfo Lean.BinderInfo.implicit) : Lean.MetaM Lean.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.

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

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

fun _ : Unit => a

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

@[inline]

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

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

@[inline]

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

@[inline]

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

@[inline]

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

@[inline]

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

withDefault x excutes x using the default transparency setting.

@[inline]

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

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

@[inline]

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

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

@[inline]

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

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

@[inline]

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

Execute x allowing isDefEq to assign synthetic opaque metavariables.

@[inline]

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

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

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

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

def Lean.Meta.isClass? (type : Lean.Expr) : Lean.MetaM (Option Lake.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)

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

def Lean.Meta.forallTelescope {n : Type → Type u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (type : Lean.Expr) (k : Array Lean.Expr → Lean.Expr → n α) : 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.

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

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

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

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

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

Similar to lambdaTelescope but for lambda and let expressions.

def Lean.Meta.lambdaTelescope {n : Type → Type u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (e : Lean.Expr) (k : Array Lean.Expr → Lean.Expr → n α) : 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.

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

Return the parameter names for the given global declaration.

def Lean.Meta.forallMetaTelescope (e : Lean.Expr) (kind : optParam Lean.MetavarKind Lean.MetavarKind.natural) : Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.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

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

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

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

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

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

Similar to forallMetaTelescopeReducingAux but for lambda expressions.

partial def Lean.Meta.lambdaMetaTelescope.process (maxMVars? : optParam (Option Nat) none) (mvars : Array Lean.Expr) (bis : Array Lean.BinderInfo) (j : Nat) (type : Lean.Expr) : Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)

def Lean.Meta.withLocalDecl {n : Type → Type u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (name : Lake.Name) (bi : Lean.BinderInfo) (type : Lean.Expr) (k : Lean.Expr → n α) (kind : optParam Lean.LocalDeclKind Lean.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.

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

def Lean.Meta.withLocalDecls {n : Type → Type u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} [Inhabited α] (declInfos : Array (Lake.Name × Lean.BinderInfo × (Array Lean.Expr → n Lean.Expr))) (k : Array Lean.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.

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

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

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

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

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

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

Add the local declaration : := 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.

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

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

Register any local instance in decls

def Lean.Meta.withExistingLocalDecls {n : Type → Type u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (decls : List Lean.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 commes with a local declarations (corresponding to pattern variables), and we use withExistingLocalDecls to add them to the local context before we process them.

def Lean.Meta.withNewMCtxDepth {n : Type → Type u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (k : n α) (allowLevelAssignments : optParam 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.)

def Lean.Meta.withLCtx {n : Type → Type u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (lctx : Lean.LocalContext) (localInsts : Lean.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.

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

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

@[deprecated Lean.MVarId.withContext]

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

def Lean.Meta.withMCtx {n : Type → Type u_1} [MonadControlT Lean.MetaM n] [Monad n] {α : Type} (mctx : Lean.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.

@[inline]

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

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

@[inline]

def Lean.Meta.fullApproxDefEq {n : Type → Type u_1} [MonadControlT Lean.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)]

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

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

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

whnf with reducible transparency.

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

whnf with default transparency.

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

whnf with instances transparency.

def Lean.Meta.setInlineAttribute (declName : Lake.Name) (kind : optParam Lean.Compiler.InlineAttributeKind Lean.Compiler.InlineAttributeKind.inline) : Lean.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.

def Lean.Meta.instantiateForall (e : Lean.Expr) (ps : Array Lean.Expr) : Lean.MetaM Lean.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].

def Lean.Meta.instantiateLambda (e : Lean.Expr) (ps : Array Lean.Expr) : Lean.MetaM Lean.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

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

Pretty-print the given expression.

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

Pretty-print the given expression.

@[inline]

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

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

instance Lean.Meta.instAlternativeMetaM : Alternative Lean.MetaM

@[inline]

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

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

Execute x, and apply f to the produced error message

@[inline]

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

def Lean.Meta.sortFVarIds (fvarIds : Array Lean.FVarId) : Lean.MetaM (Array Lean.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.

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

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

def Lean.Meta.isListLevelDefEqAux : List Lean.Level → List Lean.Level → Lean.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 : Lean.MetaM Nat

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

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

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

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

partial def Lean.Meta.processPostponed.loop (mayPostpone : optParam Bool true) (exceptionOnFailure : optParam Bool false) : Lean.MetaM Bool

@[specialize #[]]

def Lean.Meta.checkpointDefEq (x : Lean.MetaM Bool) (mayPostpone : optParam Bool true) : Lean.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.

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

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

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

See isDefEq.

@[inline, reducible]

abbrev Lean.Meta.isDefEq (t : Lean.Expr) (s : Lean.Expr) : Lean.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?

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

@[inline, reducible]

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

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

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

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

Eta expand the given expression. Example:

etaExpand (mkConst ``Nat.add)

produces fun x y => Nat.add x y