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.
Equations
- Lean.Meta.TransparencyMode.all.toUInt64 = 0
- Lean.Meta.TransparencyMode.default.toUInt64 = 1
- Lean.Meta.TransparencyMode.reducible.toUInt64 = 2
- Lean.Meta.TransparencyMode.instances.toUInt64 = 3
Instances For
Equations
- Lean.Meta.EtaStructMode.all.toUInt64 = 0
- Lean.Meta.EtaStructMode.notClasses.toUInt64 = 1
- Lean.Meta.EtaStructMode.none.toUInt64 = 2
Instances For
Configuration for projection reduction. See whnfCore
.
- no: Lean.Meta.ProjReductionKind
Projections
s.i
are not reduced atwhnfCore
. - yes: Lean.Meta.ProjReductionKind
Projections
s.i
are reduced atwhnfCore
, andwhnfCore
is used ats
during the process. Recall thatwhnfCore
does not performdelta
reduction (i.e., it will not unfold constant declarations). - yesWithDelta: Lean.Meta.ProjReductionKind
- yesWithDeltaI: Lean.Meta.ProjReductionKind
Projections
s.i
are reduced atwhnfCore
, andwhnfAtMostI
is used ats
during the process. Recall thatwhnfAtMostI
is likewhnf
but uses transparency at mostinstances
. This option is stronger thanyes
, but weaker thanyesWithDelta
. We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations. When unifying e.g.(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1
, we only want to unify negation (and not all other field operations as well). Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986
Instances For
Equations
- Lean.Meta.instDecidableEqProjReductionKind x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯
Equations
- Lean.Meta.instReprProjReductionKind = { reprPrec := Lean.Meta.reprProjReductionKind✝ }
Equations
- Lean.Meta.ProjReductionKind.no.toUInt64 = 0
- Lean.Meta.ProjReductionKind.yes.toUInt64 = 1
- Lean.Meta.ProjReductionKind.yesWithDelta.toUInt64 = 2
- Lean.Meta.ProjReductionKind.yesWithDeltaI.toUInt64 = 3
Instances For
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
a₁ ... aₙ
are pairwise distinct free variables that are not let-variables.a₁ ... aₙ
are not inC
t
only contains free variables inC
and/or{a₁, ..., aₙ}
- For every metavariable
?m'@C'
occurring int
,C'
is a subprefix ofC
?m
does not occur int
- foApprox : Bool
If
foApprox
is set to true, and someaᵢ
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 andc
is not an application as - isDefEqStuckEx : Bool
When the following flag is set,
isDefEq
throws the exceptionException.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 asexact t
. When elaboratingt
, 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 oft
with the goal target type. We claim this is not a hack and is defensible behavior because this last unification step is not really part of the term elaboration. - offsetCnstrs : Bool
Enable/Disable support for offset constraints such as
?x + 1 =?= e
- transparency : Lean.Meta.TransparencyMode
- trackZetaDelta : Bool
When
trackZetaDelta = true
, we track all free variables that have been zetaDelta-expanded. That is, suppose the local context contains the declarationx : t := v
, and we reducex
tov
, then we insertx
intoState.zetaDeltaFVarIds
. We usetrackZetaDelta
to discover which let-declarationslet x := v; e
can be represented as(fun x => e) v
. When we find these declarations we set theirnonDep
flag withtrue
. To find these let-declarations in a given terms
, we 1- ResetState.zetaDeltaFVarIds
2- SettrackZetaDelta := true
3- Type-checks
. - etaStruct : Lean.Meta.EtaStructMode
Eta for structures configuration mode.
- univApprox : Bool
When
univApprox
is set to true, we use approximations when solving postponed universe constraints. Examples:max u ?v =?= u
is solved with?v := u
and ignoring the solution?v := 0
.max u w =?= mav u ?v
is solved with?v := w
ignoring the solution?v := max u w
- iota : Bool
- beta : Bool
If
true
, reduce terms such as(fun x => t[x]) a
intot[a]
- proj : Lean.Meta.ProjReductionKind
Control projection reduction at
whnfCore
. - zeta : Bool
Zeta reduction:
let x := v; e[x]
reduces toe[v]
. We say a let-declarationlet x := v; e
is non dependent if it is equivalent to(fun x => e) v
. Recall thatfun x : BitVec 5 => let n := 5; fun y : BitVec n => x = y
is type correct, but
fun x : BitVec 5 => (fun n => fun y : BitVec n => x = y) 5
is not.
- zetaDelta : Bool
Zeta-delta reduction: given a local context containing entry
x : t := e
, free variablex
reduces toe
.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Meta.instInhabitedConfigWithKey = { default := { config := default, key := default } }
Equations
- c.toConfigWithKey = { config := c, key := Lean.Meta.Config.toKey✝ c }
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
contains the backwards dependencies. That is, the (0-indexed) position of previous parameters that this one depends on.- isProp : Bool
isProp
is true if the parameter type is always a proposition. - isDecInst : Bool
- 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
sincedom
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
- p.isImplicit = (p.binderInfo == Lean.BinderInfo.implicit)
Instances For
Equations
- p.isInstImplicit = (p.binderInfo == Lean.BinderInfo.instImplicit)
Instances For
Equations
- p.isStrictImplicit = (p.binderInfo == Lean.BinderInfo.strictImplicit)
Instances For
Equations
- p.isExplicit = (p.binderInfo == Lean.BinderInfo.default)
Instances For
Function information cache. See ParamInfo
.
- paramInfo : Array Lean.Meta.ParamInfo
Parameter information cache.
resultDeps
contains the function result type backwards dependencies. That is, the (0-indexed) position of parameters that the result type depends on.
Instances For
Equations
- Lean.Meta.instInhabitedInfoCacheKey = { default := { configKey := default, expr := default, nargs? := default } }
Equations
Equations
- One or more equations did not get rendered due to their size.
- localInsts : Lean.LocalInstances
- type : Lean.Expr
- synthPendingDepth : Nat
Value of
synthPendingDepth
when instance was synthesized or failed to be synthesized. See issue #2522.
Instances For
Equations
- Lean.Meta.instInhabitedAbstractMVarsResult = { default := { paramNames := default, numMVars := default, expr := default } }
Equations
Instances For
Equations
- Lean.Meta.instInhabitedExprConfigCacheKey = { default := { expr := default, configKey := default } }
Equations
- Lean.Meta.instBEqExprConfigCacheKey = { beq := fun (a b : Lean.Meta.ExprConfigCacheKey) => a.expr.equal b.expr && a.configKey == b.configKey }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Instances For
Instances For
Equations
- Lean.Meta.instInhabitedDefEqCacheKey = { default := { lhs := default, rhs := default, configKey := default } }
Equations
Equations
- One or more equations did not get rendered due to their size.
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.
Instances For
Cache datastructures for type inference, type class resolution, whnf, and definitional equality.
- inferType : Lean.Meta.InferTypeCache
- funInfo : Lean.Meta.FunInfoCache
- synthInstance : Lean.Meta.SynthInstanceCache
- whnf : Lean.Meta.WhnfCache
- defEqTrans : Lean.Meta.DefEqCache
- defEqPerm : Lean.Meta.DefEqCache
Instances For
Equations
- Lean.Meta.instInhabitedCache = { default := { inferType := default, funInfo := default, synthInstance := default, whnf := default, defEqTrans := default, defEqPerm := default } }
"Context" for a postponed universe constraint.
lhs
and rhs
are the surrounding isDefEq
call when the postponed constraint was created.
- lhs : Lean.Expr
- rhs : Lean.Expr
- lctx : Lean.LocalContext
- localInstances : Lean.LocalInstances
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.
- 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 the entry was created.
Instances For
Equations
- Lean.Meta.instInhabitedPostponedEntry = { default := { ref := default, lhs := default, rhs := default, ctx? := default } }
- unfoldCounter : Lean.PHashMap Lean.Name Nat
Number of times each declaration has been unfolded
- heuristicCounter : Lean.PHashMap Lean.Name Nat
Number of times
f a =?= f b
heuristic has been used per functionf
. - instanceCounter : Lean.PHashMap Lean.Name Nat
Number of times a TC instance is used.
- synthPendingFailures : Lean.PHashMap Lean.Expr Lean.MessageData
Pending instances that were not synthesized because
maxSynthPendingDepth
has been reached.
Instances For
Equations
- Lean.Meta.instInhabitedDiagnostics = { default := { unfoldCounter := default, heuristicCounter := default, instanceCounter := default, synthPendingFailures := default } }
MetaM
monad state.
- mctx : Lean.MetavarContext
- cache : Lean.Meta.Cache
- zetaDeltaFVarIds : Lean.FVarIdSet
When
trackZetaDelta == true
, then any let-decl free variable that is zetaDelta-expanded byMetaM
is stored inzetaDeltaFVarIds
. - postponed : Lean.PersistentArray Lean.Meta.PostponedEntry
Array of postponed universe level constraints
- diag : Lean.Meta.Diagnostics
Instances For
Equations
- Lean.Meta.instInhabitedState = { default := { mctx := default, cache := default, zetaDeltaFVarIds := default, postponed := default, diag := default } }
Backtrackable state for the MetaM
monad.
- core : Lean.Core.SavedState
- meta : Lean.Meta.State
Instances For
Contextual information for the MetaM
monad.
- config : Lean.Meta.Config
- configKey : UInt64
- lctx : Lean.LocalContext
Local context
- localInstances : Lean.LocalInstances
Local instances in
lctx
. - defEqCtx? : Option Lean.Meta.DefEqContext
Not
none
when inside of anisDefEq
test. SeePostponedEntry
. - synthPendingDepth : Nat
Track the number of nested
synthPending
invocations. Nested invocations can happen when the type class resolution invokessynthPending
.Remark:
synthPending
fails ifsynthPendingDepth > maxSynthPendingDepth
. - 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 atwhnf
whencanUnfold?
is notnone
. - univApprox : Bool
When
Config.univApprox := true
, this flag is set totrue
when there is no progress processing universe constraints. - inTypeClassResolution : Bool
inTypeClassResolution := true
whenisDefEq
is invoked attryResolve
in the type class resolution module. We don't useisDefEqProjDelta
when performing TC resolution due to performance issues. This is not a great solution, but a proper solution would require a more sophisticased caching mechanism.
Instances For
The MetaM
monad is a core component of Lean's metaprogramming framework, facilitating the
construction and manipulation of expressions (Lean.Expr
) within Lean.
It builds on top of CoreM
and additionally provides:
- A
LocalContext
for managing free variables. - A
MetavarContext
for managing metavariables. - A
Cache
for caching results of the keyMetaM
operations.
The key operations provided by MetaM
are:
inferType
, which attempts to automatically infer the type of a given expression.whnf
, which reduces an expression to the point where the outermost part is no longer reducible but the inside may still contain unreduced expression.isDefEq
, which determines whether two expressions are definitionally equal, possibly assigning meta variables in the process.forallTelescope
andlambdaTelescope
, which make it possible to automatically move into (nested) binders while updating the local context.
The following is a small example that demonstrates how to obtain and manipulate the type of a
Fin
expression:
import Lean
open Lean Meta
def getFinBound (e : Expr) : MetaM (Option Expr) := do
let type ← whnf (← inferType e)
let_expr Fin bound := type | return none
return bound
def a : Fin 100 := 42
run_meta
match ← getFinBound (.const ``a []) with
| some limit => IO.println (← ppExpr limit)
| none => IO.println "no limit found"
Equations
Instances For
Equations
- Lean.Meta.instMonadMetaM = Monad.mk
Equations
- Lean.Meta.instInhabitedMetaM = { default := fun (x : Lean.Meta.Context) (x : ST.Ref IO.RealWorld Lean.Meta.State) => default }
Equations
- Lean.Meta.instMonadLCtxMetaM = { getLCtx := do let __do_lift ← read pure __do_lift.lctx }
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
- Lean.Meta.instAddMessageContextMetaM = { addMessageContext := Lean.addMessageContextFull }
Equations
- Lean.Meta.saveState = do let __do_lift ← liftM Lean.Core.saveState let __do_lift_1 ← get pure { core := __do_lift, meta := __do_lift_1 }
Instances For
Restore backtrackable parts of the state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Incremental reuse primitive: if reusableResult?
is none
, runs act
and returns its result
together with the saved monadic state after act
including the heartbeats used by it. If
reusableResult?
on the other hand is some (a, state)
, restores full state
including heartbeats
used and returns (a, state)
.
The intention is for steps that support incremental reuse to initially pass none
as
reusableResult?
and store the result and state in a snapshot. In a further run, if reuse is
possible, reusableResult?
should be set to the previous result and state, ensuring that the state
after running withRestoreOrSaveFull
is identical in both runs. Note however that necessarily this
is only an approximation in the case of heartbeats as heartbeats used by withRestoreOrSaveFull
itself after calling act
as well as by reuse-handling code such as the one supplying
reusableResult?
are not accounted for.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.instMonadBacktrackSavedStateMetaM = { saveState := Lean.Meta.saveState, restoreState := fun (s : Lean.Meta.SavedState) => s.restore }
Equations
- x.run ctx s = (x ctx).run s
Instances For
Instances For
Equations
Instances For
Equations
- Lean.Meta.throwIsDefEqStuck = throw (Lean.Exception.internal Lean.Meta.isDefEqStuckExceptionId)
Instances For
Equations
Instances For
Equations
- Lean.Meta.mapMetaM f x = controlAt Lean.MetaM fun (runInBase : {β : Type} → m β → Lean.MetaM (stM Lean.MetaM m β)) => f (runInBase x)
Instances For
Equations
- Lean.Meta.map1MetaM f k = controlAt Lean.MetaM fun (runInBase : {β : Type} → m β → Lean.MetaM (stM Lean.MetaM m β)) => f fun (b : β) => runInBase (k b)
Instances For
Equations
- Lean.Meta.map2MetaM f k = controlAt Lean.MetaM fun (runInBase : {β : Type} → m β → Lean.MetaM (stM Lean.MetaM m β)) => f fun (b : β) (c : γ) => runInBase (k b c)
Instances For
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
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
Equations
- Lean.Meta.mkExprConfigCacheKey expr = do let __do_lift ← read pure { expr := expr, configKey := Lean.Meta.Context.configKey✝ __do_lift }
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.mkInfoCacheKey expr nargs? = do let __do_lift ← read pure { configKey := Lean.Meta.Context.configKey✝ __do_lift, expr := expr, nargs? := nargs? }
Instances For
Equations
- Lean.Meta.resetDefEqPermCaches = Lean.Meta.modifyDefEqPermCache fun (x : Lean.Meta.DefEqCache) => { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray }
Instances For
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
If diagnostics are enabled, record that declName
has been unfolded.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If diagnostics are enabled, record that heuristic for solving f a =?= f b
has been used.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If diagnostics are enabled, record that instance declName
was used during TC resolution.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If diagnostics are enabled, record that synth pending failures.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.getLocalInstances = do let __do_lift ← read pure __do_lift.localInstances
Instances For
Equations
- Lean.Meta.getConfig = do let __do_lift ← read pure (Lean.Meta.Context.config✝ __do_lift)
Instances For
Equations
- Lean.Meta.getConfigWithKey = do let __do_lift ← Lean.Meta.getConfig pure __do_lift.toConfigWithKey
Instances For
Equations
- Lean.Meta.resetZetaDeltaFVarIds = modify fun (s : Lean.Meta.State) => { mctx := s.mctx, cache := s.cache, zetaDeltaFVarIds := ∅, postponed := s.postponed, diag := s.diag }
Instances For
Equations
- Lean.Meta.getZetaDeltaFVarIds = do let __do_lift ← get pure __do_lift.zetaDeltaFVarIds
Instances For
Return the array of postponed universe level constraints.
Equations
- Lean.Meta.getPostponed = do let __do_lift ← get pure __do_lift.postponed
Instances For
Set the array of postponed universe level constraints.
Equations
- Lean.Meta.setPostponed postponed = modify fun (s : Lean.Meta.State) => { mctx := s.mctx, cache := s.cache, zetaDeltaFVarIds := s.zetaDeltaFVarIds, postponed := postponed, diag := s.diag }
Instances For
Modify the array of postponed universe level constraints.
Equations
- Lean.Meta.modifyPostponed f = modify fun (s : Lean.Meta.State) => { mctx := s.mctx, cache := s.cache, zetaDeltaFVarIds := s.zetaDeltaFVarIds, postponed := f s.postponed, diag := s.diag }
Instances For
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.Ref
s in the past, it was safer but less efficient.
Reduces an expression to its weak head normal form. This is when the "head" of the top-level expression has been fully reduced. The result may contain subexpressions that have not been reduced.
See Lean.Meta.whnfImp
for the implementation.
Returns the inferred type of the given expression. Assumes the expression is type-correct.
The type inference algorithm does not do general type checking.
Type inference only looks at subterms that are necessary for determining an expression's type,
and as such if inferType
succeeds it does not mean the term is type-correct.
If an expression is sufficiently ill-formed that it prevents inferType
from computing a type,
then it will fail with a type error.
For typechecking during elaboration, see Lean.Meta.check
.
(Note that we do not guarantee that the elaborator typechecker is as correct or as efficient as
the kernel typechecker. The kernel typechecker is invoked when a definition is added to the environment.)
Here are examples of type-incorrect terms for which inferType
succeeds:
import Lean
open Lean Meta
/--
`@id.{1} Bool Nat.zero`.
In general, the type of `@id α x` is `α`.
-/
def e1 : Expr := mkApp2 (.const ``id [1]) (.const ``Bool []) (.const ``Nat.zero [])
#eval inferType e1
-- Lean.Expr.const `Bool []
#eval check e1
-- error: application type mismatch
/--
`let x : Int := Nat.zero; true`.
In general, the type of `let x := v; e`, if `e` does not reference `x`, is the type of `e`.
-/
def e2 : Expr := .letE `x (.const ``Int []) (.const ``Nat.zero []) (.const ``true []) false
#eval inferType e2
-- Lean.Expr.const `Bool []
#eval check e2
-- error: invalid let declaration
Here is an example of a type-incorrect term that makes inferType
fail:
/--
`Nat.zero Nat.zero`
-/
def e3 : Expr := .app (.const ``Nat.zero []) (.const ``Nat.zero [])
#eval inferType e3
-- error: function expected
See Lean.Meta.inferTypeImp
for the implementation of inferType
.
Equations
- Lean.Meta.whnfForall e = do let e' ← Lean.Meta.whnf e if e'.isForall = true then pure e' else pure e
Instances For
Equations
- Lean.Meta.withIncRecDepth x = Lean.Meta.mapMetaM (fun {α : Type} => Lean.withIncRecDepth) x
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.mkFreshLevelMVar = do let mvarId ← Lean.mkFreshLMVarId Lean.modifyMCtx fun (mctx : Lean.MetavarContext) => mctx.addLevelMVarDecl mvarId pure (Lean.mkLevelMVar mvarId)
Instances For
Equations
- Lean.Meta.mkFreshExprMVar type? kind userName = Lean.Meta.mkFreshExprMVarImpl✝ type? kind userName
Instances For
Equations
- Lean.Meta.mkFreshTypeMVar kind userName = do let u ← Lean.Meta.mkFreshLevelMVar Lean.Meta.mkFreshExprMVar (some (Lean.mkSort u)) kind userName
Instances For
Equations
- One or more equations did not get rendered due to their size.
- Lean.Meta.mkFreshExprMVarWithId mvarId (some type) kind userName = Lean.Meta.mkFreshExprMVarWithIdCore✝ mvarId type kind userName
Instances For
Equations
- Lean.Meta.mkFreshLevelMVars num = num.foldM (fun (x : Nat) (x : x < num) (us : List Lean.Level) => do let __do_lift ← Lean.Meta.mkFreshLevelMVar pure (__do_lift :: us)) []
Instances For
Equations
- Lean.Meta.mkFreshLevelMVarsFor info = Lean.Meta.mkFreshLevelMVars info.numLevelParams
Instances For
Create a constant with the given name and new universe metavariables.
Example: mkConstWithFreshMVarLevels `Monad
returns @Monad.{?u, ?v}
Equations
- Lean.Meta.mkConstWithFreshMVarLevels declName = do let info ← Lean.getConstInfo declName let __do_lift ← Lean.Meta.mkFreshLevelMVarsFor info pure (Lean.mkConst declName __do_lift)
Instances For
Return current transparency setting/mode.
Equations
- Lean.Meta.getTransparency = do let __do_lift ← Lean.Meta.getConfig pure __do_lift.transparency
Instances For
Equations
- Lean.Meta.shouldReduceAll = do let __do_lift ← Lean.Meta.getTransparency pure (__do_lift == Lean.Meta.TransparencyMode.all)
Instances For
Equations
- Lean.Meta.shouldReduceReducibleOnly = do let __do_lift ← Lean.Meta.getTransparency pure (__do_lift == Lean.Meta.TransparencyMode.reducible)
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.
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
Return mvarId
kind. Throw an exception if mvarId
is not declared in the current metavariable context.
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
- mvarId.setKind kind = Lean.modifyMCtx fun (mctx : Lean.MetavarContext) => mctx.setMVarKind mvarId kind
Instances For
Update the type of the given metavariable. This function assumes the new type is definitionally equal to the current one
Equations
- mvarId.setType type = Lean.modifyMCtx fun (mctx : Lean.MetavarContext) => mctx.setMVarType mvarId type
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
Returns true if mvarId.isReadOnly
returns true or if mvarId
is a synthetic opaque metavariable.
Recall isDefEq
will not assign a value to mvarId
if mvarId.isReadOnlyOrSyntheticOpaque
.
Equations
- One or more equations did not get rendered due to their size.
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
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
Set the user-facing name for the given metavariable.
Equations
- mvarId.setUserName newUserName = Lean.modifyMCtx fun (mctx : Lean.MetavarContext) => mctx.setMVarUserName mvarId newUserName
Instances For
Throw an exception saying fvarId
is not declared in the current local context.
Equations
- fvarId.throwUnknown = Lean.throwError (Lean.toMessageData "unknown free variable '" ++ Lean.toMessageData (Lean.mkFVar fvarId) ++ Lean.toMessageData "'")
Instances For
Return some decl
if fvarId
is declared in the current local context.
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
Return the type of the given free variable.
Instances For
Return the binder information for the given free variable.
Instances For
Return some value
if the given free variable is a let-declaration, and none
otherwise.
Instances For
Return the user-facing name for the given free variable.
Instances For
Return true
is the free variable is a let-variable.
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
- Lean.Meta.getFVarLocalDecl fvar = fvar.fvarId!.getDecl
Instances For
Returns true
if another local declaration in the local context depends on fvarId
.
Equations
- One or more equations did not get rendered due to their size.
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
- Lean.Meta.getFVarFromUserName userName = do let d ← Lean.Meta.getLocalDeclFromUserName userName pure (Lean.Expr.fvar d.fvarId)
Instances For
Lift a MkBindingM
monadic action x
to MetaM
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
- e.abstractRangeM n xs = Lean.Meta.liftMkBindingM (Lean.MetavarContext.abstractRange e n xs)
Instances For
Replace free (or meta) variables xs
with loose bound variables.
Similar to Expr.abstract
, but handles metavariables correctly.
Equations
- e.abstractM xs = e.abstractRangeM xs.size xs
Instances For
Collect forward dependencies for the free variables in toRevert
.
Recall that when reverting free variables xs
, we must also revert their forward dependencies.
Equations
- Lean.Meta.collectForwardDeps toRevert preserveOrder = Lean.Meta.liftMkBindingM (Lean.MetavarContext.collectForwardDeps toRevert preserveOrder)
Instances For
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 asusedOnly
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
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
Equations
- Lean.Meta.mkLetFVars xs e usedLetOnly binderInfoForMVars = Lean.Meta.mkLambdaFVars xs e false usedLetOnly false binderInfoForMVars
Instances For
fun _ : Unit => a
Equations
- Lean.Meta.mkFunUnit a = do let __do_lift ← liftM (Lean.mkFreshUserName `x) pure (Lean.mkLambda __do_lift Lean.BinderInfo.default (Lean.mkConst `Unit) a)
Instances For
Equations
- Lean.Meta.elimMVarDeps xs e preserveOrder = if xs.isEmpty = true then pure e else Lean.Meta.liftMkBindingM (Lean.MetavarContext.elimMVarDeps xs e preserveOrder)
Instances For
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
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
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
Executes x
tracking zetaDelta reductions Config.trackZetaDelta := true
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
Equations
- Lean.Meta.withTransparency mode = Lean.Meta.mapMetaM fun {α : Type} => withReader fun (x : Lean.Meta.Context) => Lean.Meta.Context.setTransparency✝ x mode
Instances For
withDefault x
executes x
using the default transparency setting.
Instances For
withReducible x
executes x
using the reducible transparency setting. In this setting only definitions tagged as [reducible]
are unfolded.
Equations
Instances For
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
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
Execute x
allowing isDefEq
to assign synthetic opaque metavariables.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.savingCache = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.savingCacheImpl✝
Instances For
Equations
- Lean.Meta.getTheoremInfo info = do let __do_lift ← Lean.Meta.shouldReduceAll if __do_lift = true then pure (some info) else pure none
Instances For
Add entry { className := className, fvar := fvar }
to localInstances,
and then execute continuation k
.
Equations
- Lean.Meta.withNewLocalInstance className fvar = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withNewLocalInstanceImp✝ className fvar
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
Equations
- Lean.Meta.withNewLocalInstances fvars j = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withNewLocalInstancesImpAux✝ fvars j
Instances For
Given type
of the form forall xs, A
, execute k xs A
.
This combinator will declare local declarations, create free variables for them,
execute k
with updated local context, and make sure the cache is restored after executing k
.
If cleanupAnnotations
is true
, we apply Expr.cleanupAnnotations
to each type in the telescope.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Given a monadic function f
that takes a term and produces a new term,
lifts this to the monadic function that opens a ∀
telescope, applies f
to the body,
and then builds the lambda telescope term for the new term.
Equations
- Lean.Meta.mapForallTelescope f forallTerm = Lean.Meta.mapForallTelescope' (fun (x e : Lean.Expr) => f e) forallTerm
Instances For
Similar to forallTelescope
, but given type
of the form forall xs, A
,
it reduces A
and continues building the telescope if it is a forall
.
If cleanupAnnotations
is true
, we apply Expr.cleanupAnnotations
to each type in the telescope.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Similar to forallTelescopeReducing
, stops constructing the telescope when
it reaches size maxFVars
.
If cleanupAnnotations
is true
, we apply Expr.cleanupAnnotations
to each type in the telescope.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
Given e
of the form fun ..xs ..ys => A
, execute k xs (fun ..ys => A)
where
xs.size ≤ maxFVars
.
This combinator will declare local declarations, create free variables for them,
execute k
with updated local context, and make sure the cache is restored after executing k
.
If cleanupAnnotations
is true
, we apply Expr.cleanupAnnotations
to each type in the telescope.
Equations
- One or more equations did not get rendered due to their size.
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
- Lean.Meta.forallMetaTelescope e kind = Lean.Meta.forallMetaTelescopeReducingAux✝ e false none kind
Instances For
Similar to forallMetaTelescope
, but if e = forall ..xs, A
it will reduce A
to construct further mvars.
Equations
- Lean.Meta.forallMetaTelescopeReducing e maxMVars? kind = Lean.Meta.forallMetaTelescopeReducingAux✝ e true maxMVars? kind
Instances For
Similar to forallMetaTelescopeReducing
, stops
constructing the telescope when it reaches size maxMVars
.
Equations
- Lean.Meta.forallMetaBoundedTelescope e maxMVars kind = Lean.Meta.forallMetaTelescopeReducingAux✝ e true (some maxMVars) kind
Instances For
Similar to forallMetaTelescopeReducingAux
but for lambda expressions.
Equations
- Lean.Meta.lambdaMetaTelescope e maxMVars? = Lean.Meta.lambdaMetaTelescope.process maxMVars? #[] #[] 0 e
Instances For
Create a free variable x
with name, binderInfo and type, add it to the context and run in k
.
Then revert the context.
Equations
- Lean.Meta.withLocalDecl name bi type k kind = Lean.Meta.map1MetaM (fun {α : Type} (k : Lean.Expr → Lean.MetaM α) => Lean.Meta.withLocalDeclImp✝ name bi type k kind) k
Instances For
Equations
- Lean.Meta.withLocalDeclD name type k = Lean.Meta.withLocalDecl name Lean.BinderInfo.default type k
Instances For
Similar to withLocalDecl
, but it does not check whether the new variable is a local instance or not.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
- Lean.Meta.withLocalDecls declInfos k = Lean.Meta.withLocalDecls.loop declInfos k #[]
Instances For
Equations
- Lean.Meta.withNewBinderInfos bs k = Lean.Meta.mapMetaM (fun {α : Type} (k : Lean.MetaM α) => Lean.Meta.withNewBinderInfosImp✝ bs k) k
Instances For
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
Add the local declaration <name> : <type> := <val>
to the local context and execute k x
, where x
is a new
free variable corresponding to the let
-declaration. After executing k x
, the local context is restored.
Equations
- Lean.Meta.withLetDecl name type val k kind = Lean.Meta.map1MetaM (fun {α : Type} (k : Lean.Expr → Lean.MetaM α) => Lean.Meta.withLetDeclImp✝ name type val k kind) k
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Register any local instance in decls
Equations
- Lean.Meta.withLocalInstances decls = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withLocalInstancesImp decls
Instances For
withExistingLocalDecls decls k
, adds the given local declarations to the local context,
and then executes k
. This method assumes declarations in decls
have valid FVarId
s.
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
- Lean.Meta.withExistingLocalDecls decls = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withExistingLocalDeclsImp✝ decls
Instances For
Removes fvarId
from the local context, and replaces occurrences of it with e
.
It is the responsibility of the caller to ensure that e
is well-typed in the context
of any occurrence of fvarId
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
withNewMCtxDepth k
executes k
with a higher metavariable context depth,
where metavariables created outside the withNewMCtxDepth
(with a lower depth) cannot be assigned.
If allowLevelAssignments
is set to true, then the level metavariable depth
is not increased, and level metavariables from the outer scope can be
assigned. (This is used by TC synthesis.)
Equations
- Lean.Meta.withNewMCtxDepth k allowLevelAssignments = Lean.Meta.mapMetaM (fun {α : Type} => Lean.Meta.withNewMCtxDepthImp✝ allowLevelAssignments) k
Instances For
withLCtx lctx localInsts k
replaces the local context and local instances, and then executes k
.
The local context and instances are restored after executing k
.
This method assumes that the local instances in localInsts
are in the local context lctx
.
Equations
- Lean.Meta.withLCtx lctx localInsts = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withLocalContextImp✝ lctx localInsts
Instances For
Simpler version of withLCtx
which just updates the local context. It is the resposability of the
caller ensure the local instances are also properly updated.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Runs k
in a local environment with the fvarIds
erased.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
- mvarId.withContext = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withMVarContextImp✝ mvarId
Instances For
withMCtx mctx k
replaces the metavariable context and then executes k
.
The metavariable context is restored after executing k
.
This method is used to implement the type class resolution procedure.
Equations
- Lean.Meta.withMCtx mctx = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withMCtxImp✝ mctx
Instances For
Execute x
using approximate unification: foApprox
, ctxApprox
and quasiPatternApprox
.
Equations
- Lean.Meta.approxDefEq = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.approxDefEqImp✝
Instances For
Similar to approxDefEq
, but uses all available approximations.
We don't use constApprox
by default at approxDefEq
because it often produces undesirable solution for monadic code.
For example, suppose we have pure (x > 0)
which has type ?m Prop
. We also have the goal [Pure ?m]
.
Now, assume the expected type is IO Bool
. Then, the unification constraint ?m Prop =?= IO Bool
could be solved
as ?m := fun _ => IO Bool
using constApprox
, but this spurious solution would generate a failure when we try to
solve [Pure (fun _ => IO Bool)]
Equations
- Lean.Meta.fullApproxDefEq = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.fullApproxDefEqImp✝
Instances For
Instantiate assigned universe metavariables in u
, and then normalize it.
Equations
- Lean.Meta.normalizeLevel u = do let u ← Lean.instantiateLevelMVars u pure u.normalize
Instances For
whnf
with at most instances transparency.
Equations
- One or more equations did not get rendered due to their size.
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
- Lean.Meta.ppExpr e = (fun (x : Lean.FormatWithInfos) => x.fmt) <$> Lean.Meta.ppExprWithInfos e
Instances For
Equations
- Lean.Meta.orElse x y = do let s ← Lean.saveState tryCatch x fun (x : Lean.Exception) => do s.restore y ()
Instances For
Equations
- Lean.Meta.instOrElseMetaM = { orElse := Lean.Meta.orElse }
Equations
- Lean.Meta.instAlternativeMetaM = Alternative.mk (fun {x : Type} => Lean.throwError (Lean.toMessageData "failed")) fun {α : Type} => Lean.Meta.orElse
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
Execute x
, and apply f
to the produced error message
Equations
- Lean.Meta.mapErrorImp x f = tryCatch x fun (ex : Lean.Exception) => match ex with | Lean.Exception.error ref msg => throw (Lean.Exception.error ref (f msg)) | ex => throw ex
Instances For
Equations
- Lean.Meta.mapError x f = controlAt Lean.MetaM fun (runInBase : {β : Type} → m β → Lean.MetaM (stM Lean.MetaM m β)) => Lean.Meta.mapErrorImp (runInBase x) f
Instances For
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
- 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
Instances For
Equations
- Lean.Meta.getNumPostponed = do let __do_lift ← Lean.Meta.getPostponed pure __do_lift.size
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Meta.mkLevelStuckErrorMessage entry = Lean.Meta.mkLevelErrorMessageCore✝ "stuck at solving universe constraint" entry
Instances For
Equations
- Lean.Meta.mkLevelErrorMessage entry = Lean.Meta.mkLevelErrorMessageCore✝ "failed to solve universe constraint" entry
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Determines whether two expressions are definitionally equal to each other.
To control how metavariables are assigned and unified, metavariables and their context have a "depth".
Given a metavariable ?m
and a MetavarContext
mctx
, ?m
is not assigned if ?m.depth != mctx.depth
.
The combinator withNewMCtxDepth x
will bump the depth while executing x
.
So, withNewMCtxDepth (isDefEq a b)
is isDefEq
without any mvar assignment happening
whereas isDefEq a b
will assign any metavariables of the current depth in a
and b
to unify them.
For matching (where only mvars in b
should be assigned), we create the term inside the withNewMCtxDepth
.
For an example, see Lean.Meta.Simp.tryTheoremWithExtraArgs?
Equations
- Lean.Meta.isDefEq t s = Lean.Meta.isExprDefEq t s
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Similar to isDefEq
, but returns false
if an exception has been thrown.
Equations
Instances For
Equations
Instances For
Returns true
if mvarId := val
was successfully assigned.
This method uses the same assignment validation performed by isDefEq
, but it does not check whether the types match.
If e
is of the form ?m ...
instantiate metavars
Equations
- Lean.Meta.instantiateMVarsIfMVarApp e = if e.getAppFn.isMVar = true then Lean.instantiateMVars e else pure e