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
a₁ ... aₙare pairwise distinct free variables that are not let-variables.a₁ ... aₙare not inCtonly contains free variables inCand/or{a₁, ..., aₙ}- For every metavariable
?m'@C'occurring int,C'is a subprefix ofC ?mdoes not occur int
- foApprox : Bool
If
foApproxis 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_kreduces to
?m a_1 ... a_i =?= f a_{i+1} =?= b_1 ... a_{i+k} =?= b_k - ctxApprox : Bool
When
ctxApproxis set to true, we relax condition 4, by creating an auxiliary metavariable?n'with a smaller context than?m'. - quasiPatternApprox : Bool
When
quasiPatternApproxis set to true, we ignore condition 2. - constApprox : Bool
When
constApproxis set to true, we solve?m t =?= cusing?m := fun _ => cwhen?m tis not a higher-order pattern andcis not an application as - isDefEqStuckEx : Bool
When the following flag is set,
isDefEqthrows the exceptionExeption.isDefEqStuckwhenever it encounters a constraint?m ... =?= twhere?mis 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 oftwith 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 reducextov, then we insertxintoState.zetaDeltaFVarIds. We usetrackZetaDeltato discover which let-declarationslet x := v; ecan be represented as(fun x => e) v. When we find these declarations we set theirnonDepflag withtrue. To find these let-declarations in a given terms, we 1- ResetState.zetaDeltaFVarIds2- SettrackZetaDelta := true3- Type-checks. - etaStruct : Lean.Meta.EtaStructMode
Eta for structures configuration mode.
Function parameter information cache.
- binderInfo : Lean.BinderInfo
The binder annotation for the parameter.
- hasFwdDeps : Bool
hasFwdDepsis true if there is another parameter whose type depends on this one. backDepscontains the backwards dependencies. That is, the (0-indexed) position of previous parameters that this one depends on.- isProp : Bool
isPropis true if the parameter is always a proposition. - isDecInst : Bool
- higherOrderOutParam : Bool
higherOrderOutParamis 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 → elemThis flag is true for the parameter
dombecause it is output parameter of[self : GetElem cont idx elem dom] - dependsOnHigherOrderOutParam : Bool
dependsOnHigherOrderOutParamis 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 → elemThis flag is true for the parameter with type
dom xs isincedomis 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
- Lean.Meta.ParamInfo.isImplicit p = (p.binderInfo == Lean.BinderInfo.implicit)
Equations
- Lean.Meta.ParamInfo.isInstImplicit p = (p.binderInfo == Lean.BinderInfo.instImplicit)
Equations
- Lean.Meta.ParamInfo.isStrictImplicit p = (p.binderInfo == Lean.BinderInfo.strictImplicit)
Equations
- Lean.Meta.ParamInfo.isExplicit p = (p.binderInfo == Lean.BinderInfo.default)
Function information cache. See ParamInfo.
- paramInfo : Array Lean.Meta.ParamInfo
Parameter information cache.
resultDepscontains the function result type backwards dependencies. That is, the (0-indexed) position of parameters that the result type depends on.
Key for the function information cache.
- transparency : Lean.Meta.TransparencyMode
The transparency mode used to compute the
FunInfo. - expr : Lean.Expr
The function being cached information about. It is quite often an
Expr.const.
Equations
- Lean.Meta.instInhabitedInfoCacheKey = { default := { transparency := default, expr := default, nargs? := default } }
Equations
Equations
- One or more equations did not get rendered due to their size.
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 : Lean.PersistentHashMap (Lean.Expr × Lean.Expr) Bool
- instances : Lean.PersistentHashMap (Lean.Expr × Lean.Expr) Bool
- default : Lean.PersistentHashMap (Lean.Expr × Lean.Expr) Bool
- all : Lean.PersistentHashMap (Lean.Expr × Lean.Expr) Bool
Instances For
Equations
- Lean.Meta.instInhabitedDefEqCache = { default := { reducible := default, instances := default, default := default, all := default } }
Cache datastructures for type inference, type class resolution, whnf, and definitional equality.
- inferType : Lean.Meta.InferTypeCache
- funInfo : Lean.Meta.FunInfoCache
- synthInstance : Lean.Meta.SynthInstanceCache
- whnfDefault : Lean.Meta.WhnfCache
- whnfAll : Lean.Meta.WhnfCache
- defEqTrans : Lean.Meta.DefEqCache
- defEqPerm : Lean.Meta.DefEqCache
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.
- lhs : Lean.Expr
- rhs : Lean.Expr
- lctx : Lean.LocalContext
- localInstances : Lean.LocalInstances
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
refat 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
isDefEqcall when the entry was created.
Instances For
Equations
- Lean.Meta.instInhabitedPostponedEntry = { default := { ref := default, lhs := default, rhs := default, ctx? := 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 byMetaMis stored inzetaDeltaFVarIds. - postponed : Lean.PersistentArray Lean.Meta.PostponedEntry
Array of postponed universe level constraints
Instances For
Equations
- Lean.Meta.instInhabitedState = { default := { mctx := default, cache := default, zetaDeltaFVarIds := default, postponed := default } }
Backtrackable state for the MetaM monad.
- core : Lean.Core.State
- meta : Lean.Meta.State
Contextual information for the MetaM monad.
- config : Lean.Meta.Config
- lctx : Lean.LocalContext
Local context
- localInstances : Lean.LocalInstances
Local instances in
lctx. - defEqCtx? : Option Lean.Meta.DefEqContext
Not
nonewhen inside of anisDefEqtest. SeePostponedEntry. - synthPendingDepth : Nat
Track the number of nested
synthPendinginvocations. Nested invocations can happen when the type class resolution invokessynthPending.Remark: in the current implementation,
synthPendingfails ifsynthPendingDepth > 0. We will add a configuration option if necessary. - canUnfold? : Option (Lean.Meta.Config → Lean.ConstantInfo → Lean.CoreM Bool)
A predicate to control whether a constant can be unfolded or not at
whnf. Note that we do not cache results atwhnfwhencanUnfold?is notnone.
Equations
Instances For
- Lean.Meta.instAddMessageContextMetaM
- Lean.Meta.instAlternativeMetaM
- Lean.Meta.instInhabitedMetaM
- Lean.Meta.instMetaEvalMetaM
- Lean.Meta.instMonadBacktrackSavedStateMetaM
- Lean.Meta.instMonadEnvMetaM
- Lean.Meta.instMonadLCtxMetaM
- Lean.Meta.instMonadMCtxMetaM
- Lean.Meta.instMonadMetaM
- Lean.Meta.instOrElseMetaM
- Mathlib.Meta.NormNum.instMonadLiftOptionMetaM
Equations
- Lean.Meta.instMonadMetaM = let i := inferInstanceAs (Monad Lean.MetaM); 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 ← getThe Lean.Core.State let __do_lift_1 ← get pure { core := __do_lift, meta := __do_lift_1 }
Restore backtrackable parts of the state.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Meta.instMonadBacktrackSavedStateMetaM = { saveState := Lean.Meta.saveState, restoreState := fun (s : Lean.Meta.SavedState) => Lean.Meta.SavedState.restore s }
Equations
- Lean.Meta.MetaM.run x ctx s = StateRefT'.run (x ctx) s
Equations
- Lean.Meta.MetaM.run' x ctx s = Prod.fst <$> Lean.Meta.MetaM.run x ctx s
Equations
- Lean.Meta.MetaM.toIO x ctxCore sCore ctx s = do let __discr ← Lean.Core.CoreM.toIO (Lean.Meta.MetaM.run x ctx s) ctxCore sCore match __discr with | ((a, s), sCore) => pure (a, sCore, s)
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Meta.throwIsDefEqStuck = throw (Lean.Exception.internal Lean.Meta.isDefEqStuckExceptionId)
Equations
Equations
- Lean.Meta.mapMetaM f x = controlAt Lean.MetaM fun (runInBase : {β : Type} → m β → Lean.MetaM (stM Lean.MetaM m β)) => f (runInBase x)
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)
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)
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
- 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
- One or more equations did not get rendered due to their size.
Equations
- Lean.Meta.getLocalInstances = do let __do_lift ← read pure __do_lift.localInstances
Equations
- Lean.Meta.getConfig = do let __do_lift ← read pure __do_lift.config
Equations
- Lean.Meta.resetZetaDeltaFVarIds = modify fun (s : Lean.Meta.State) => { mctx := s.mctx, cache := s.cache, zetaDeltaFVarIds := ∅, postponed := s.postponed }
Equations
- Lean.Meta.getZetaDeltaFVarIds = do let __do_lift ← get pure __do_lift.zetaDeltaFVarIds
Return the array of postponed universe level constraints.
Equations
- Lean.Meta.getPostponed = do let __do_lift ← get pure __do_lift.postponed
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 }
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 }
useEtaStruct inductName return true if we eta for structures is enabled for
for the inductive datatype inductName.
Recall we have three different settings: .none (never use it), .all (always use it), .notClasses
(enabled only for structure-like inductive types that are not classes).
The parameter inductName affects the result only if the current setting is .notClasses.
Equations
- One or more equations did not get rendered due to their size.
WARNING: The following 4 constants are a hack for simulating forward declarations.
They are defined later using the export attribute. This is hackish because we
have to hard-code the true arity of these definitions here, and make sure the C names match.
We have used another hack based on IO.Refs in the past, it was safer but less efficient.
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.
Returns the inferred type of the given expression, or fails if it is not type-correct.
Equations
- Lean.Meta.whnfForall e = do let e' ← Lean.Meta.whnf e if Lean.Expr.isForall e' = true then pure e' else pure e
Equations
- Lean.Meta.withIncRecDepth x = Lean.Meta.mapMetaM (fun {α : Type} => Lean.withIncRecDepth) x
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.mkFreshExprMVar type? kind userName = Lean.Meta.mkFreshExprMVarImpl type? kind userName
Equations
- Lean.Meta.mkFreshTypeMVar kind userName = do let u ← Lean.Meta.mkFreshLevelMVar Lean.Meta.mkFreshExprMVar (some (Lean.mkSort u)) kind userName
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Meta.mkFreshLevelMVars num = Nat.foldM (fun (x : Nat) (us : List Lean.Level) => do let __do_lift ← Lean.Meta.mkFreshLevelMVar pure (__do_lift :: us)) [] num
Equations
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)
Return current transparency setting/mode.
Equations
- Lean.Meta.getTransparency = do let __do_lift ← Lean.Meta.getConfig pure __do_lift.transparency
Equations
- Lean.Meta.shouldReduceAll = do let __do_lift ← Lean.Meta.getTransparency pure (__do_lift == Lean.Meta.TransparencyMode.all)
Equations
- Lean.Meta.shouldReduceReducibleOnly = do let __do_lift ← Lean.Meta.getTransparency pure (__do_lift == Lean.Meta.TransparencyMode.reducible)
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
- Lean.MVarId.findDecl? mvarId = do let __do_lift ← Lean.getMCtx pure (Lean.MetavarContext.findDecl? __do_lift mvarId)
Equations
- Lean.Meta.findMVarDecl? mvarId = Lean.MVarId.findDecl? mvarId
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.
Equations
- Lean.Meta.getMVarDecl mvarId = Lean.MVarId.getDecl mvarId
Return mvarId kind. Throw an exception if mvarId is not declared in the current metavariable context.
Equations
- Lean.MVarId.getKind mvarId = do let __do_lift ← Lean.MVarId.getDecl mvarId pure __do_lift.kind
Equations
- Lean.Meta.getMVarDeclKind mvarId = Lean.MVarId.getKind mvarId
Return true if e is a synthetic (or synthetic opaque) metavariable
Equations
- One or more equations did not get rendered due to their size.
Set mvarId kind in the current metavariable context.
Equations
- Lean.MVarId.setKind mvarId kind = Lean.modifyMCtx fun (mctx : Lean.MetavarContext) => Lean.MetavarContext.setMVarKind mctx mvarId kind
Equations
- Lean.Meta.setMVarKind mvarId kind = Lean.MVarId.setKind mvarId kind
Update the type of the given metavariable. This function assumes the new type is definitionally equal to the current one
Equations
- Lean.MVarId.setType mvarId type = Lean.modifyMCtx fun (mctx : Lean.MetavarContext) => Lean.MetavarContext.setMVarType mctx mvarId type
Equations
- Lean.Meta.setMVarType mvarId type = Lean.MVarId.setType mvarId type
Return true if the given metavariable is "read-only".
That is, its depth is different from the current metavariable context depth.
Equations
- Lean.MVarId.isReadOnly mvarId = do let __do_lift ← Lean.MVarId.getDecl mvarId let __do_lift_1 ← Lean.getMCtx pure (__do_lift.depth != __do_lift_1.depth)
Equations
- Lean.Meta.isReadOnlyExprMVar mvarId = Lean.MVarId.isReadOnly mvarId
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.
Equations
Return the level of the given universe level metavariable.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Meta.getLevelMVarDepth mvarId = Lean.LMVarId.getLevel mvarId
Return true if the given universe metavariable is "read-only".
That is, its depth is different from the current metavariable context depth.
Equations
- Lean.LMVarId.isReadOnly mvarId = do let __do_lift ← Lean.LMVarId.getLevel mvarId let __do_lift_1 ← Lean.getMCtx pure (decide (__do_lift < __do_lift_1.levelAssignDepth))
Equations
- Lean.Meta.isReadOnlyLevelMVar mvarId = Lean.LMVarId.isReadOnly mvarId
Set the user-facing name for the given metavariable.
Equations
- Lean.MVarId.setUserName mvarId newUserName = Lean.modifyMCtx fun (mctx : Lean.MetavarContext) => Lean.MetavarContext.setMVarUserName mctx mvarId newUserName
Equations
- Lean.Meta.setMVarUserName mvarId userNameNew = Lean.MVarId.setUserName mvarId userNameNew
Throw an exception saying fvarId is not declared in the current local context.
Equations
- Lean.FVarId.throwUnknown fvarId = Lean.throwError (Lean.toMessageData "unknown free variable '" ++ Lean.toMessageData (Lean.mkFVar fvarId) ++ Lean.toMessageData "'")
Equations
- Lean.Meta.throwUnknownFVar fvarId = liftM (Lean.FVarId.throwUnknown fvarId)
Return some decl if fvarId is declared in the current local context.
Equations
- Lean.FVarId.findDecl? fvarId = do let __do_lift ← Lean.getLCtx pure (Lean.LocalContext.find? __do_lift fvarId)
Equations
- Lean.Meta.findLocalDecl? fvarId = Lean.FVarId.findDecl? fvarId
Return the local declaration for the given free variable. Throw an exception if local declaration is not in the current local context.
Equations
- Lean.FVarId.getDecl fvarId = do let __do_lift ← Lean.getLCtx match Lean.LocalContext.find? __do_lift fvarId with | some d => pure d | none => liftM (Lean.FVarId.throwUnknown fvarId)
Equations
- Lean.Meta.getLocalDecl fvarId = Lean.FVarId.getDecl fvarId
Return the type of the given free variable.
Equations
- Lean.FVarId.getType fvarId = do let __do_lift ← Lean.FVarId.getDecl fvarId pure (Lean.LocalDecl.type __do_lift)
Return the binder information for the given free variable.
Equations
- Lean.FVarId.getBinderInfo fvarId = do let __do_lift ← Lean.FVarId.getDecl fvarId pure (Lean.LocalDecl.binderInfo __do_lift)
Return some value if the given free variable is a let-declaration, and none otherwise.
Equations
- Lean.FVarId.getValue? fvarId = do let __do_lift ← Lean.FVarId.getDecl fvarId pure (Lean.LocalDecl.value? __do_lift)
Return the user-facing name for the given free variable.
Equations
- Lean.FVarId.getUserName fvarId = do let __do_lift ← Lean.FVarId.getDecl fvarId pure (Lean.LocalDecl.userName __do_lift)
Return true is the free variable is a let-variable.
Equations
- Lean.FVarId.isLetVar fvarId = do let __do_lift ← Lean.FVarId.getDecl fvarId pure (Lean.LocalDecl.isLet __do_lift)
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
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.
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 (Lean.LocalDecl.fvarId d))
Lift a MkBindingM monadic action x to MetaM.
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- Lean.Meta.abstractRange e n xs = Lean.Expr.abstractRangeM e n xs
Replace free (or meta) variables xs with loose bound variables.
Similar to Expr.abstract, but handles metavariables correctly.
Equations
- Lean.Expr.abstractM e xs = Lean.Expr.abstractRangeM e (Array.size xs) xs
Equations
- Lean.Meta.abstract e xs = Lean.Expr.abstractM e xs
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)
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 = truethen only variables that the expression body depends on will appear. - if
usedLetOnly = truesame asusedOnlyexcept 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.
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.
Equations
- Lean.Meta.mkLetFVars xs e usedLetOnly binderInfoForMVars = Lean.Meta.mkLambdaFVars xs e false usedLetOnly binderInfoForMVars
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)
Equations
- Lean.Meta.elimMVarDeps xs e preserveOrder = if Array.isEmpty xs = true then pure e else Lean.Meta.liftMkBindingM (Lean.MetavarContext.elimMVarDeps xs e preserveOrder)
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.
Executes x tracking zetaDelta reductions Config.trackZetaDelta := true
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
- One or more equations did not get rendered due to their size.
withDefault x executes x using the default transparency setting.
withReducible x executes x using the reducible transparency setting. In this setting only definitions tagged as [reducible] are unfolded.
withReducibleAndInstances x executes x using the .instances transparency setting. In this setting only definitions tagged as [reducible]
or type class instances are unfolded.
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.
Execute x allowing isDefEq to assign synthetic opaque metavariables.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Meta.savingCache = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.savingCacheImpl
Equations
- Lean.Meta.getTheoremInfo info = do let __do_lift ← Lean.Meta.shouldReduceAll if __do_lift = true then pure (some info) else pure none
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
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.
Equations
- Lean.Meta.withNewLocalInstances fvars j = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withNewLocalInstancesImpAux fvars j
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
- Lean.Meta.forallTelescope type k = Lean.Meta.map2MetaM (fun {α : Type} (k : Array Lean.Expr → Lean.Expr → Lean.MetaM α) => Lean.Meta.forallTelescopeImp type k) k
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.
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
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
- Lean.Meta.forallTelescopeReducing type k = Lean.Meta.map2MetaM (fun {α : Type} (k : Array Lean.Expr → Lean.Expr → Lean.MetaM α) => Lean.Meta.forallTelescopeReducingImp type k) k
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.
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.
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.
Return the parameter names for the given global declaration.
Equations
- One or more equations did not get rendered due to their size.
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
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
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
Similar to forallMetaTelescopeReducingAux but for lambda expressions.
Equations
- Lean.Meta.lambdaMetaTelescope e maxMVars? = Lean.Meta.lambdaMetaTelescope.process maxMVars? #[] #[] 0 e
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
Equations
- Lean.Meta.withLocalDeclD name type k = Lean.Meta.withLocalDecl name Lean.BinderInfo.default type k
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 #[]
Equations
- Lean.Meta.withNewBinderInfos bs k = Lean.Meta.mapMetaM (fun {α : Type} (k : Lean.MetaM α) => Lean.Meta.withNewBinderInfosImp bs k) 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.
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
Equations
- One or more equations did not get rendered due to their size.
Register any local instance in decls
Equations
- Lean.Meta.withLocalInstances decls = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withLocalInstancesImp decls
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
- Lean.Meta.withExistingLocalDecls decls = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withExistingLocalDeclsImp decls
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
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
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
- Lean.MVarId.withContext mvarId = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.withMVarContextImp mvarId
Equations
- Lean.Meta.withMVarContext mvarId = Lean.MVarId.withContext mvarId
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
Execute x using approximate unification: foApprox, ctxApprox and quasiPatternApprox.
Equations
- Lean.Meta.approxDefEq = Lean.Meta.mapMetaM fun {α : Type} => Lean.Meta.approxDefEqImp
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
Instantiate assigned universe metavariables in u, and then normalize it.
Equations
- Lean.Meta.normalizeLevel u = do let u ← Lean.instantiateLevelMVars u pure (Lean.Level.normalize u)
whnf with reducible transparency.
whnf with default transparency.
whnf with instances transparency.
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.
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
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
Pretty-print the given expression.
Equations
- One or more equations did not get rendered due to their size.
Pretty-print the given expression.
Equations
- Lean.Meta.ppExpr e = (fun (x : Lean.FormatWithInfos) => x.fmt) <$> Lean.Meta.ppExprWithInfos e
Equations
- Lean.Meta.orElse x y = do let s ← Lean.saveState tryCatch x fun (x : Lean.Exception) => do Lean.Meta.SavedState.restore s y ()
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.
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
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
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.
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.
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
Equations
- Lean.Meta.getNumPostponed = do let __do_lift ← Lean.Meta.getPostponed pure __do_lift.size
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Meta.mkLevelStuckErrorMessage entry = Lean.Meta.mkLeveErrorMessageCore "stuck at solving universe constraint" entry
Equations
- Lean.Meta.mkLevelErrorMessage entry = Lean.Meta.mkLeveErrorMessageCore "failed to solve universe constraint" entry
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.
Determines whether two universe level expressions are definitionally equal to each other.
Equations
See isDefEq.
Equations
- One or more equations did not get rendered due to their size.
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
Equations
- One or more equations did not get rendered due to their size.
Similar to isDefEq, but returns false if an exception has been thrown.
Equations
Equations
If e is of the form ?m ... instantiate metavars
Equations
- Lean.Meta.instantiateMVarsIfMVarApp e = if Lean.Expr.isMVar (Lean.Expr.getAppFn e) = true then Lean.instantiateMVars e else pure e