Documentation

Lean.Meta.Basic

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.

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

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

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 (fun x => e) v. 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.

• Eta for structures configuration mode.

Instances For

Function parameter information cache.

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

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]

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

Function information cache. See ParamInfo.

• paramInfo :

Parameter information cache.

• resultDeps :

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

Instances For

Key for the function information cache.

• 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? :

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

Instances For
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
@[inline, reducible]
Equations
Instances For
@[inline, reducible]
Equations
Instances For
@[inline, reducible]
Equations
Instances For
@[inline, reducible]
Equations
Instances For

A mapping (s, t) ↦ isDefEq s t per transparency level. 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.

• reducible :
• instances :
• default :
Instances For
Equations

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

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

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

Instances For

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.

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

• ctx? :

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

Instances For
Equations

MetaM monad state.

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

• postponed :

Array of postponed universe level constraints

Instances For
Equations

Backtrackable state for the MetaM monad.

Instances For

Contextual information for the MetaM monad.

• Local context

• localInstances : Lean.LocalInstances

Local instances in lctx.

• defEqCtx? :

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? :

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.

Instances For
@[inline, reducible]
abbrev Lean.Meta.MetaM (α : Type) :
Equations
Instances For
@[always_inline]
Equations
Equations
• Lean.Meta.instInhabitedMetaM = { default := fun (x : Lean.Meta.Context) (x : ) => default }
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations
Instances For

Restore backtrackable parts of the state.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline]
def Lean.Meta.MetaM.run {α : Type} (x : ) (ctx : optParam Lean.Meta.Context { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true, transparency := Lean.Meta.TransparencyMode.default, trackZetaDelta := false, etaStruct := Lean.Meta.EtaStructMode.all }, lctx := { fvarIdToDecl := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := , tail := , 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 }, defEqTrans := { reducible := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, instances := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, default := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, all := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, defEqPerm := { reducible := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, instances := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, default := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, all := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }, zetaDeltaFVarIds := , postponed := { root := , tail := , size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }) :
Equations
Instances For
@[inline]
def Lean.Meta.MetaM.run' {α : Type} (x : ) (ctx : optParam Lean.Meta.Context { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true, transparency := Lean.Meta.TransparencyMode.default, trackZetaDelta := false, etaStruct := Lean.Meta.EtaStructMode.all }, lctx := { fvarIdToDecl := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := , tail := , 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 }, defEqTrans := { reducible := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, instances := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, default := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, all := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, defEqPerm := { reducible := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, instances := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, default := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, all := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }, zetaDeltaFVarIds := , postponed := { root := , tail := , size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }) :
Equations
Instances For
@[inline]
def Lean.Meta.MetaM.toIO {α : Type} (x : ) (ctxCore : Lean.Core.Context) (sCore : Lean.Core.State) (ctx : optParam Lean.Meta.Context { config := { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false, isDefEqStuckEx := false, unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true, transparency := Lean.Meta.TransparencyMode.default, trackZetaDelta := false, etaStruct := Lean.Meta.EtaStructMode.all }, lctx := { fvarIdToDecl := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := , tail := , 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 }, defEqTrans := { reducible := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, instances := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, default := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, all := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, defEqPerm := { reducible := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, instances := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, default := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, all := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } } }, zetaDeltaFVarIds := , postponed := { root := , tail := , size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }) :
Equations
Instances For
instance Lean.Meta.instMetaEvalMetaM {α : Type} [] :
Equations
• One or more equations did not get rendered due to their size.
Equations
• Lean.Meta.throwIsDefEqStuck =
Instances For
@[inline]
def Lean.Meta.liftMetaM {m : TypeType u_1} {α : Type} [] (x : ) :
m α
Equations
Instances For
@[inline]
def Lean.Meta.mapMetaM {m : TypeType u_1} [] (f : {α : Type} → ) {α : Type} (x : m α) :
m α
Equations
Instances For
@[inline]
def Lean.Meta.map1MetaM {m : TypeType u_1} {β : Sort u_2} [] (f : {α : Type} → (β)) {α : Type} (k : βm α) :
m α
Equations
Instances For
@[inline]
def Lean.Meta.map2MetaM {m : TypeType u_1} {β : Sort u_2} {γ : Sort u_3} [] (f : {α : Type} → (βγ)) {α : Type} (k : βγm α) :
m α
Equations
Instances For
@[inline]
Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline]
Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline]
Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline]
Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline]
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For
Equations
Instances For

Return the array of postponed universe level constraints.

Equations
Instances For
def Lean.Meta.setPostponed (postponed : ) :

Set the array of postponed universe level constraints.

Equations
Instances For
@[inline]

Modify the array of postponed universe level constraints.

Equations
• = modify fun (s : Lean.Meta.State) => { mctx := s.mctx, cache := s.cache, zetaDeltaFVarIds := s.zetaDeltaFVarIds, postponed := f s.postponed }
Instances For
def Lean.Meta.useEtaStruct (inductName : Lake.Name) :

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.
Instances For

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]

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]

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

@[extern 7 lean_is_expr_def_eq]
@[extern 7 lean_is_level_def_eq]
@[extern 6 lean_synth_pending]
Equations
Instances For
def Lean.Meta.withIncRecDepth {n : TypeType u_1} [] {α : Type} (x : n α) :
n α
Equations
Instances For
def Lean.Meta.mkFreshExprMVarAt (lctx : Lean.LocalContext) (localInsts : Lean.LocalInstances) (type : Lean.Expr) (userName : ) (numScopeArgs : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
def Lean.Meta.mkFreshExprMVar (type? : ) (userName : ) :
Equations
Instances For
Equations
Instances For
def Lean.Meta.mkFreshExprMVarWithId (mvarId : Lean.MVarId) (type? : optParam none) (userName : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For

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

Equations
Instances For

Return current transparency setting/mode.

Equations
Instances For
Equations
Instances For

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
Instances For
@[deprecated Lean.MVarId.findDecl?]
Equations
Instances For

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.
Instances For
@[deprecated Lean.MVarId.getDecl]
Equations
Instances For

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

Equations
Instances For
@[deprecated Lean.MVarId.getKind]
Equations
Instances For

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

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

Set mvarId kind in the current metavariable context.

Equations
Instances For
@[deprecated Lean.MVarId.setKind]
Equations
Instances For
def Lean.MVarId.setType (mvarId : Lean.MVarId) (type : Lean.Expr) :

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

Equations
Instances For
@[deprecated Lean.MVarId.setType]
def Lean.Meta.setMVarType (mvarId : Lean.MVarId) (type : Lean.Expr) :
Equations
Instances For

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

Equations
Instances For
Equations
Instances For

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.

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

Return the level of the given universe level metavariable.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[deprecated Lean.LMVarId.getLevel]
Equations
Instances For

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

Equations
Instances For
Equations
Instances For

Set the user-facing name for the given metavariable.

Equations
Instances For
Equations
Instances For
def Lean.FVarId.throwUnknown {α : Type} (fvarId : Lean.FVarId) :

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

Equations
Instances For
@[deprecated Lean.FVarId.throwUnknown]
Equations
Instances For

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

Equations
Instances For
@[deprecated Lean.FVarId.findDecl?]
Equations
Instances For

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

Equations
Instances For
@[deprecated Lean.FVarId.getDecl]
Equations
Instances For

Return the type of the given free variable.

Equations
Instances For

Return the binder information for the given free variable.

Equations
Instances For

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

Equations
Instances For

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

Equations
Instances For

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

Equations
Instances For

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
Instances For

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.
Instances For

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

Equations
Instances For
@[inline]

Lift a MkBindingM monadic action x to MetaM.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Lean.Expr.abstractRangeM (e : Lean.Expr) (n : Nat) (xs : ) :

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.

Equations
Instances For
@[deprecated Lean.Expr.abstractRangeM]
def Lean.Meta.abstractRange (e : Lean.Expr) (n : Nat) (xs : ) :
Equations
Instances For
def Lean.Expr.abstractM (e : Lean.Expr) (xs : ) :

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

Equations
Instances For
@[deprecated Lean.Expr.abstractM]
def Lean.Meta.abstract (e : Lean.Expr) (xs : ) :
Equations
Instances For
def Lean.Meta.collectForwardDeps (toRevert : ) (preserveOrder : Bool) :

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

Equations
Instances For
def Lean.Meta.mkForallFVars (xs : ) (e : Lean.Expr) (usedOnly : ) (usedLetOnly : ) (binderInfoForMVars : ) :

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.)
Equations
• One or more equations did not get rendered due to their size.
Instances For
def Lean.Meta.mkLambdaFVars (xs : ) (e : Lean.Expr) (usedOnly : ) (usedLetOnly : ) (binderInfoForMVars : ) :

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.
Instances For
def Lean.Meta.mkLetFVars (xs : ) (e : Lean.Expr) (usedLetOnly : ) (binderInfoForMVars : ) :
Equations
Instances For

fun _ : Unit => a

Equations
Instances For
def Lean.Meta.elimMVarDeps (xs : ) (e : Lean.Expr) (preserveOrder : ) :
Equations
Instances For
@[inline]
def Lean.Meta.withConfig {n : TypeType u_1} [] {α : Type} (f : ) :
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.
Instances For
@[inline]
def Lean.Meta.withTrackingZetaDelta {n : TypeType u_1} [] {α : Type} (x : n α) :
n α

Executes x tracking zetaDelta reductions Config.trackZetaDelta := true

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline]
def Lean.Meta.withoutProofIrrelevance {n : TypeType u_1} [] {α : Type} (x : n α) :
n α
Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline]
def Lean.Meta.withTransparency {n : TypeType u_1} [] {α : Type} (mode : Lean.Meta.TransparencyMode) :
n αn α
Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline]
def Lean.Meta.withDefault {n : TypeType u_1} [] {α : Type} (x : n α) :
n α

withDefault x executes x using the default transparency setting.

Equations
Instances For
@[inline]
def Lean.Meta.withReducible {n : TypeType u_1} [] {α : Type} (x : n α) :
n α

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

Equations
Instances For
@[inline]
def Lean.Meta.withReducibleAndInstances {n : TypeType u_1} [] {α : 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
Instances For
@[inline]
def Lean.Meta.withAtLeastTransparency {n : TypeType u_1} [] {α : Type} (mode : Lean.Meta.TransparencyMode) (x : 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.
Instances For
@[inline]
def Lean.Meta.withAssignableSyntheticOpaque {n : TypeType u_1} [] {α : 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.
Instances For
@[inline]
def Lean.Meta.savingCache {n : TypeType u_1} [] {α : Type} :
n αn α
Equations
Instances For
Equations
Instances For
def Lean.Meta.withNewLocalInstance {n : TypeType u_1} [] {α : Type} (className : Lake.Name) (fvar : Lean.Expr) :
n αn α

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

Equations
Instances For

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.
Instances For
def Lean.Meta.withNewLocalInstances {n : TypeType u_1} [] {α : Type} (fvars : ) (j : Nat) :
n αn α
Equations
Instances For
def Lean.Meta.forallTelescope {n : TypeType u_1} [] {α : Type} (type : Lean.Expr) (k : Lean.Exprn α) :
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.

Equations
Instances For
def Lean.Meta.mapForallTelescope' (f : ) (forallTerm : Lean.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.
Instances For
def Lean.Meta.mapForallTelescope (f : ) (forallTerm : Lean.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
Instances For
def Lean.Meta.forallTelescopeReducing {n : TypeType u_1} [] {α : Type} (type : Lean.Expr) (k : Lean.Exprn α) :
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.

Equations
Instances For
def Lean.Meta.forallBoundedTelescope {n : TypeType u_1} [] {α : Type} (type : Lean.Expr) (maxFVars? : ) (k : Lean.Exprn α) :
n α

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def Lean.Meta.lambdaLetTelescope {n : TypeType u_1} [] {α : Type} (e : Lean.Expr) (k : Lean.Exprn α) (cleanupAnnotations : ) :
n α

Similar to lambdaTelescope but for lambda and let expressions.

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.
Instances For
def Lean.Meta.lambdaTelescope {n : TypeType u_1} [] {α : Type} (e : Lean.Expr) (k : Lean.Exprn α) (cleanupAnnotations : ) :
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.
Instances For

Return the parameter names for the given global declaration.

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

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
Instances For
def Lean.Meta.forallMetaTelescopeReducing (e : Lean.Expr) (maxMVars? : optParam () none) :

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

Equations
Instances For

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

Equations
Instances For
def Lean.Meta.lambdaMetaTelescope (e : Lean.Expr) (maxMVars? : optParam () none) :

Similar to forallMetaTelescopeReducingAux but for lambda expressions.

Equations
Instances For
partial def Lean.Meta.lambdaMetaTelescope.process (maxMVars? : optParam () none) (mvars : ) (bis : ) (j : Nat) (type : Lean.Expr) :
def Lean.Meta.withLocalDecl {n : TypeType u_1} [] {α : Type} (name : Lake.Name) (bi : Lean.BinderInfo) (type : Lean.Expr) (k : Lean.Exprn α) :
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
Instances For
def Lean.Meta.withLocalDeclD {n : TypeType u_1} [] {α : Type} (name : Lake.Name) (type : Lean.Expr) (k : Lean.Exprn α) :
n α
Equations
Instances For
def Lean.Meta.withLocalDecls {n : TypeType u_1} [] {α : Type} [] (declInfos : Array ()) (k : 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.
Equations
Instances For
partial def Lean.Meta.withLocalDecls.loop {n : TypeType u_1} [] {α : Type} (declInfos : Array ()) (k : n α) [] (acc : ) :
n α
def Lean.Meta.withLocalDeclsD {n : TypeType u_1} [] {α : Type} [] (declInfos : Array ()) (k : n α) :
n α
Equations
• One or more equations did not get rendered due to their size.
Instances For
def Lean.Meta.withNewBinderInfos {n : TypeType u_1} [] {α : Type} (bs : ) (k : n α) :
n α
Equations
Instances For
def Lean.Meta.withInstImplicitAsImplict {α : Type} (xs : ) (k : ) :

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.
Instances For
def Lean.Meta.withLetDecl {n : TypeType u_1} [] {α : Type} (name : Lake.Name) (type : Lean.Expr) (val : Lean.Expr) (k : Lean.Exprn α) :
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
Instances For
def Lean.Meta.withLocalInstancesImp {α : Type} (decls : ) (k : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
def Lean.Meta.withLocalInstances {n : TypeType u_1} [] {α : Type} (decls : ) :
n αn α

Register any local instance in decls

Equations
Instances For
def Lean.Meta.withExistingLocalDecls {n : TypeType u_1} [] {α : Type} (decls : ) :
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.

Equations
Instances For
def Lean.Meta.withNewMCtxDepth {n : TypeType u_1} [] {α : Type} (k : n α) (allowLevelAssignments : ) :
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
Instances For
def Lean.Meta.withLCtx {n : TypeType u_1} [] {α : 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.

Equations
Instances For
def Lean.MVarId.withContext {n : TypeType u_1} [] {α : 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.

Equations
Instances For
@[deprecated Lean.MVarId.withContext]
def Lean.Meta.withMVarContext {n : TypeType u_1} [] {α : Type} (mvarId : Lean.MVarId) :
n αn α
Equations
Instances For
def Lean.Meta.withMCtx {n : TypeType u_1} [] {α : 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.

Equations
Instances For
@[inline]
def Lean.Meta.approxDefEq {n : TypeType u_1} [] {α : Type} :
n αn α

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

Equations
Instances For
@[inline]
def Lean.Meta.fullApproxDefEq {n : TypeType u_1} [] {α : 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
Instances For

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

Equations
• = do let u ←
Instances For

whnf with reducible transparency.

Equations
Instances For

whnf with default transparency.

Equations
Instances For

whnf with instances transparency.

Equations
Instances For

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.
Instances For

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
Instances For

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
Instances For

Pretty-print the given expression.

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

Pretty-print the given expression.

Equations
Instances For
@[inline]
def Lean.Meta.orElse {α : Type} (x : ) (y : ) :
Equations
Instances For
Equations
• Lean.Meta.instOrElseMetaM = { orElse := Lean.Meta.orElse }
Equations
@[inline]
def Lean.Meta.orelseMergeErrors {m : TypeType u_1} {α : Type} [] (x : m α) (y : m α) (mergeRef : optParam fun (r₁ x : Lean.Syntax) => r₁) (mergeMsg : optParam fun (m₁ m₂ : Lean.MessageData) => ) :
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.
Instances For
def Lean.Meta.mapErrorImp {α : Type} (x : ) (f : ) :

Execute x, and apply f to the produced error message

Equations
Instances For
@[inline]
def Lean.Meta.mapError {m : TypeType u_1} {α : Type} [] (x : m α) (f : ) :
m α
Equations
Instances For
def Lean.Meta.sortFVarIds (fvarIds : ) :

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.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
Instances For
def Lean.Meta.processPostponed (mayPostpone : ) (exceptionOnFailure : ) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
partial def Lean.Meta.processPostponed.loop (mayPostpone : ) (exceptionOnFailure : ) :
@[specialize #[]]
def Lean.Meta.checkpointDefEq (x : ) (mayPostpone : ) :

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.
Instances For

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

Equations
Instances For

See isDefEq.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline, reducible]

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
Instances For
Equations
• One or more equations did not get rendered due to their size.
Instances For
@[inline, reducible]

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

Equations
Instances For
Equations
Instances For

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.
Instances For

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

Equations
Instances For