Lean.Meta.Basic

Type

foApprox : Bool
ctxApprox : Bool
quasiPatternApprox : 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
constApprox : Bool
When the following flag is set, isDefEq throws the exeption Exeption.isDefEqStuck whenever it encounters a constraint ?m ... =?= t where ?m is read only. This feature is useful for type class resolution where we may want to notify the caller that the TC problem may be solveable later after it assigns ?m.
isDefEqStuckEx : Bool
transparency : Lean.Meta.TransparencyMode
If zetaNonDep == false, then non dependent let-decls are not zeta expanded.
zetaNonDep : Bool
When trackZeta == true, we store zetaFVarIds all free variables that have been zeta-expanded.
trackZeta : Bool
unificationHints : Bool
Enables proof irrelevance at isDefEq
proofIrrelevance : 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.
assignSyntheticOpaque : Bool
When ignoreLevelDepth is false, only universe level metavariables with depth == metavariable context depth can be assigned. We used to have ignoreLevelDepth == false always, but this setting produced counterintuitive behavior in a few cases. Recall that universe levels are often ignored by users, they may not even be aware they exist. We still use this restriction for regular metavariables. See discussion at the beginning of MetavarContext.lean. We claim it is reasonable to ignore this restriction for universe metavariables because their values are often contrained by the terms is instances and simp theorems. TODO: we should delete this configuration option and the method isReadOnlyLevelMVar after we have more tests.
ignoreLevelMVarDepth : Bool
Enable/Disable support for offset constraints such as ?x + 1 =?= e
offsetCnstrs : Bool
Eta for structures configuration mode.
etaStruct : Lean.Meta.EtaStructMode

source

structure Lean.Meta.ParamInfo:

Type

binderInfo : Lean.BinderInfo
hasFwdDeps : Bool
backDeps : Array Nat
isProp : Bool
isDecInst : Bool

source

instance Lean.Meta.instInhabitedParamInfo:

Inhabited Lean.Meta.ParamInfo

Equations

Lean.Meta.instInhabitedParamInfo = { default := { binderInfo := default, hasFwdDeps := default, backDeps := default, isProp := default, isDecInst := default } }

source

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

Bool

Equations

Lean.Meta.ParamInfo.isImplicit p = (p.binderInfo == Lean.BinderInfo.implicit)

source

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

Bool

Equations

Lean.Meta.ParamInfo.isInstImplicit p = (p.binderInfo == Lean.BinderInfo.instImplicit)

source

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

Bool

Equations

Lean.Meta.ParamInfo.isStrictImplicit p = (p.binderInfo == Lean.BinderInfo.strictImplicit)

source

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

Bool

Equations

Lean.Meta.ParamInfo.isExplicit p = (p.binderInfo == Lean.BinderInfo.default || p.binderInfo == Lean.BinderInfo.auxDecl)

source

structure Lean.Meta.FunInfo:

Type

paramInfo : Array Lean.Meta.ParamInfo
resultDeps : Array Nat

source

structure Lean.Meta.InfoCacheKey:

Type

transparency : Lean.Meta.TransparencyMode
expr : Lean.Expr
nargs? : Option Nat

source

instance Lean.Meta.instInhabitedInfoCacheKey:

Inhabited Lean.Meta.InfoCacheKey

Equations

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

source

instance Lean.Meta.instBEqInfoCacheKey:

BEq Lean.Meta.InfoCacheKey

Equations

Lean.Meta.instBEqInfoCacheKey = { beq := [anonymous] }

source

instance Lean.Meta.InfoCacheKey.instHashableInfoCacheKey:

Hashable Lean.Meta.InfoCacheKey

Equations

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

source

@[inline]

abbrev Lean.Meta.SynthInstanceCache:

Type

Equations

Lean.Meta.SynthInstanceCache = Std.PersistentHashMap Lean.Expr (Option Lean.Expr)

source

@[inline]

abbrev Lean.Meta.InferTypeCache:

Type

Equations

Lean.Meta.InferTypeCache = Lean.PersistentExprStructMap Lean.Expr

source

@[inline]

abbrev Lean.Meta.FunInfoCache:

Type

Equations

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

source

@[inline]

abbrev Lean.Meta.WhnfCache:

Type

Equations

Lean.Meta.WhnfCache = Lean.PersistentExprStructMap Lean.Expr

source

@[inline]

abbrev Lean.Meta.DefEqCache:

Type

Equations

Lean.Meta.DefEqCache = Std.PersistentHashMap (Lean.Expr × Lean.Expr) Unit

source

structure Lean.Meta.Cache:

Type

inferType : Lean.Meta.InferTypeCache
funInfo : Lean.Meta.FunInfoCache
synthInstance : Lean.Meta.SynthInstanceCache
whnfDefault : Lean.Meta.WhnfCache
whnfAll : Lean.Meta.WhnfCache
defEqDefault : Lean.Meta.DefEqCache
defEqAll : Lean.Meta.DefEqCache

source

instance Lean.Meta.instInhabitedCache:

Inhabited Lean.Meta.Cache

Equations

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

source

structure Lean.Meta.DefEqContext:

Type

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

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

source

structure Lean.Meta.PostponedEntry:

Type

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

source

instance Lean.Meta.instInhabitedPostponedEntry:

Inhabited Lean.Meta.PostponedEntry

Equations

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

source

structure Lean.Meta.State:

Type

mctx : Lean.MetavarContext
cache : Lean.Meta.Cache
zetaFVarIds : Lean.FVarIdSet
postponed : Std.PersistentArray Lean.Meta.PostponedEntry

source

instance Lean.Meta.instInhabitedState:

Inhabited Lean.Meta.State

Equations

Lean.Meta.instInhabitedState = { default := { mctx := default, cache := default, zetaFVarIds := default, postponed := default } }

source

structure Lean.Meta.SavedState:

Type

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

source

instance Lean.Meta.instInhabitedSavedState:

Inhabited Lean.Meta.SavedState

Equations

Lean.Meta.instInhabitedSavedState = { default := { core := default, meta := default } }

source

structure Lean.Meta.Context:

Type

config : Lean.Meta.Config
lctx : Lean.LocalContext
localInstances : Lean.LocalInstances
Not none when inside of an isDefEq test. See PostponedEntry.
defEqCtx? : Option Lean.Meta.DefEqContext
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. 
```
synthPendingDepth : Nat
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.
canUnfold? : Option (Lean.Meta.Config → Lean.ConstantInfo → Lean.CoreM Bool)

source

@[inline]

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

Type

Equations

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

source

instance Lean.Meta.instMonadMetaM:

Monad Lean.MetaM

Equations

Lean.Meta.instMonadMetaM = let i := inferInstanceAs (Monad Lean.MetaM); Monad.mk

source

instance Lean.Meta.instInhabitedMetaM {α : Type} :

Inhabited (Lean.MetaM α)

Equations

Lean.Meta.instInhabitedMetaM = { default := fun x x => default }

source

instance Lean.Meta.instMonadLCtxMetaM:

Lean.MonadLCtx Lean.MetaM

Equations

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

source

instance Lean.Meta.instMonadMCtxMetaM:

Lean.MonadMCtx Lean.MetaM

Equations

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

source

instance Lean.Meta.instMonadEnvMetaM:

Lean.MonadEnv Lean.MetaM

Equations

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

source

instance Lean.Meta.instAddMessageContextMetaM:

Lean.AddMessageContext Lean.MetaM

Equations

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

source

def Lean.Meta.saveState:

Lean.MetaM Lean.Meta.SavedState

Equations

Lean.Meta.saveState = do let a ← getThe Lean.Core.State let a_1 ← get pure { core := a, meta := a_1 }

source

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

Lean.MetaM Unit

Restore backtrackable parts of the state.

Equations

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

source

instance Lean.Meta.instMonadBacktrackSavedStateMetaM:

Lean.MonadBacktrack Lean.Meta.SavedState Lean.MetaM

Equations

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

source

@[inline]

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

Lean.CoreM (α × Lean.Meta.State)

Equations

Lean.Meta.MetaM.run x ctx s = StateRefT'.run (x ctx) s

source

@[inline]

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

Lean.CoreM α

Equations

Lean.Meta.MetaM.run' x ctx s = Prod.fst <$> Lean.Meta.MetaM.run x ctx s

source

@[inline]

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

IO (α × Lean.Core.State × Lean.Meta.State)

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)

source

instance Lean.Meta.instMetaEvalMetaM {α : Type} [inst : Lean.MetaEval α] :

Lean.MetaEval (Lean.MetaM α)

Equations

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

source

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

Lean.MetaM α

Equations

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

source

@[inline]

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

m α

Equations

Lean.Meta.liftMetaM x = liftM x

source

@[inline]

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

m α

Equations

Lean.Meta.mapMetaM f x = controlAt Lean.MetaM fun runInBase => f (stM Lean.MetaM m α) (runInBase x)

source

@[inline]

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

m α

Equations

Lean.Meta.map1MetaM f k = controlAt Lean.MetaM fun runInBase => f (stM Lean.MetaM m α) fun b => runInBase (k b)

source

@[inline]

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

m α

Equations

Lean.Meta.map2MetaM f k = controlAt Lean.MetaM fun runInBase => f (stM Lean.MetaM m α) fun b c => runInBase (k b c)

source

@[inline]

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

Lean.MetaM Unit

Equations

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

source

@[inline]

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

Lean.MetaM Unit

Equations

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

source

def Lean.Meta.getLocalInstances:

Lean.MetaM Lean.LocalInstances

Equations

Lean.Meta.getLocalInstances = do let a ← read pure a.localInstances

source

def Lean.Meta.getConfig:

Lean.MetaM Lean.Meta.Config

Equations

Lean.Meta.getConfig = do let a ← read pure a.config

source

def Lean.Meta.setMCtx (mctx : Lean.MetavarContext) :

Lean.MetaM Unit

Equations

Lean.Meta.setMCtx mctx = modify fun s => { mctx := mctx, cache := s.cache, zetaFVarIds := s.zetaFVarIds, postponed := s.postponed }

source

def Lean.Meta.resetZetaFVarIds:

Lean.MetaM Unit

Equations

Lean.Meta.resetZetaFVarIds = modify fun s => { mctx := s.mctx, cache := s.cache, zetaFVarIds := ∅, postponed := s.postponed }

source

def Lean.Meta.getZetaFVarIds:

Lean.MetaM Lean.FVarIdSet

Equations

Lean.Meta.getZetaFVarIds = do let a ← get pure a.zetaFVarIds

source

def Lean.Meta.getPostponed:

Lean.MetaM (Std.PersistentArray Lean.Meta.PostponedEntry)

Equations

Lean.Meta.getPostponed = do let a ← get pure a.postponed

source

def Lean.Meta.setPostponed (postponed : Std.PersistentArray Lean.Meta.PostponedEntry) :

Lean.MetaM Unit

Equations

Lean.Meta.setPostponed postponed = modify fun s => { mctx := s.mctx, cache := s.cache, zetaFVarIds := s.zetaFVarIds, postponed := postponed }

source

@[inline]

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

Lean.MetaM Unit

Equations

Lean.Meta.modifyPostponed f = modify fun s => { mctx := s.mctx, cache := s.cache, zetaFVarIds := s.zetaFVarIds, postponed := f s.postponed }

source

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

Lean.MetaM Bool

Equations

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

source

@[extern 6 lean_whnf]

opaque Lean.Meta.whnf:

Lean.Expr → Lean.MetaM Lean.Expr

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

source

@[extern 6 lean_infer_type]

opaque Lean.Meta.inferType:

Lean.Expr → Lean.MetaM Lean.Expr

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

source

@[extern 7 lean_is_expr_def_eq]

opaque Lean.Meta.isExprDefEqAux:

Lean.Expr → Lean.Expr → Lean.MetaM Bool

source

@[extern 7 lean_is_level_def_eq]

opaque Lean.Meta.isLevelDefEqAux:

Lean.Level → Lean.Level → Lean.MetaM Bool

source

@[extern 6 lean_synth_pending]

opaque Lean.Meta.synthPending:

Lean.MVarId → Lean.MetaM Bool

source

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

Lean.MetaM Lean.Expr

Equations

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

source

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

n α

Equations

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

source

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkFreshExprMVarAt lctx localInsts type kind userName numScopeArgs = do let a ← Lean.mkFreshMVarId Lean.Meta.mkFreshExprMVarAtCore a lctx localInsts type kind userName numScopeArgs

source

def Lean.Meta.mkFreshLevelMVar:

Lean.MetaM Lean.Level

Equations

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

source

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

Lean.MetaM Lean.Expr

Equations

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

source

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

Lean.MetaM Lean.Expr

Equations

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

source

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

Lean.MetaM Lean.Expr

Equations

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

source

def Lean.Meta.mkFreshLevelMVars (num : Nat) :

Lean.MetaM (List Lean.Level)

Equations

Lean.Meta.mkFreshLevelMVars num = Nat.foldM (fun x us => do let a ← Lean.Meta.mkFreshLevelMVar pure (a :: us)) [] num

source

def Lean.Meta.mkFreshLevelMVarsFor (info : Lean.ConstantInfo) :

Lean.MetaM (List Lean.Level)

Equations

Lean.Meta.mkFreshLevelMVarsFor info = Lean.Meta.mkFreshLevelMVars (Lean.ConstantInfo.numLevelParams info)

source

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

Lean.MetaM Lean.Expr

Equations

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

source

def Lean.Meta.getTransparency:

Lean.MetaM Lean.Meta.TransparencyMode

Equations

Lean.Meta.getTransparency = do let a ← Lean.Meta.getConfig pure a.transparency

source

def Lean.Meta.shouldReduceAll:

Lean.MetaM Bool

Equations

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

source

def Lean.Meta.shouldReduceReducibleOnly:

Lean.MetaM Bool

Equations

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

source

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

Lean.MetaM Lean.MetavarDecl

Equations

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

source

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

Lean.MetaM Unit

Equations

Lean.Meta.setMVarKind mvarId kind = Lean.modifyMCtx fun mctx => Lean.MetavarContext.setMVarKind mctx mvarId kind

source

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

Lean.MetaM Unit

Equations

Lean.Meta.setMVarType mvarId type = Lean.modifyMCtx fun mctx => Lean.MetavarContext.setMVarType mctx mvarId type

source

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

Lean.MetaM Bool

Equations

Lean.Meta.isReadOnlyExprMVar mvarId = do let a ← Lean.Meta.getMVarDecl mvarId let a_1 ← Lean.getMCtx pure (a.depth != a_1.depth)

source

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

Lean.MetaM Bool

Equations

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

source

def Lean.Meta.getLevelMVarDepth (mvarId : Lean.MVarId) :

Lean.MetaM Nat

Equations

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

source

def Lean.Meta.isReadOnlyLevelMVar (mvarId : Lean.MVarId) :

Lean.MetaM Bool

Equations

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

source

def Lean.Meta.setMVarUserName (mvarId : Lean.MVarId) (newUserName : Lean.Name) :

Lean.MetaM Unit

Equations

Lean.Meta.setMVarUserName mvarId newUserName = Lean.modifyMCtx fun mctx => Lean.MetavarContext.setMVarUserName mctx mvarId newUserName

source

def Lean.Meta.isExprMVarAssigned (mvarId : Lean.MVarId) :

Lean.MetaM Bool

Equations

Lean.Meta.isExprMVarAssigned mvarId = do let a ← Lean.getMCtx pure (Lean.MetavarContext.isExprAssigned a mvarId)

source

def Lean.Meta.getExprMVarAssignment? (mvarId : Lean.MVarId) :

Lean.MetaM (Option Lean.Expr)

Equations

Lean.Meta.getExprMVarAssignment? mvarId = do let a ← Lean.getMCtx pure (Lean.MetavarContext.getExprAssignment? a mvarId)

source

def Lean.Meta.occursCheck (mvarId : Lean.MVarId) (e : Lean.Expr) :

Lean.MetaM Bool

Return true if e contains mvarId directly or indirectly

Equations

Lean.Meta.occursCheck mvarId e = do let a ← Lean.getMCtx pure (Lean.MetavarContext.occursCheck a mvarId e)

source

def Lean.Meta.assignExprMVar (mvarId : Lean.MVarId) (val : Lean.Expr) :

Lean.MetaM Unit

Equations

Lean.Meta.assignExprMVar mvarId val = Lean.modifyMCtx fun mctx => Lean.MetavarContext.assignExpr mctx mvarId val

source

def Lean.Meta.isDelayedAssigned (mvarId : Lean.MVarId) :

Lean.MetaM Bool

Equations

Lean.Meta.isDelayedAssigned mvarId = do let a ← Lean.getMCtx pure (Lean.MetavarContext.isDelayedAssigned a mvarId)

source

def Lean.Meta.getDelayedAssignment? (mvarId : Lean.MVarId) :

Lean.MetaM (Option Lean.DelayedMetavarAssignment)

Equations

Lean.Meta.getDelayedAssignment? mvarId = do let a ← Lean.getMCtx pure (Lean.MetavarContext.getDelayedAssignment? a mvarId)

source

def Lean.Meta.hasAssignableMVar (e : Lean.Expr) :

Lean.MetaM Bool

Equations

Lean.Meta.hasAssignableMVar e = do let a ← Lean.getMCtx pure (Lean.MetavarContext.hasAssignableMVar a e)

source

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

Lean.MetaM α

Equations

Lean.Meta.throwUnknownFVar fvarId = Lean.throwError (Lean.toMessageData "unknown free variable '" ++ Lean.toMessageData (Lean.mkFVar fvarId) ++ Lean.toMessageData "'")

source

def Lean.Meta.findLocalDecl? (fvarId : Lean.FVarId) :

Lean.MetaM (Option Lean.LocalDecl)

Equations

Lean.Meta.findLocalDecl? fvarId = do let a ← Lean.getLCtx pure (Lean.LocalContext.find? a fvarId)

source

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

Lean.MetaM Lean.LocalDecl

Equations

Lean.Meta.getLocalDecl fvarId = do let a ← Lean.getLCtx match Lean.LocalContext.find? a fvarId with | some d => pure d | none => Lean.Meta.throwUnknownFVar fvarId

source

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

Lean.MetaM Lean.LocalDecl

Equations

Lean.Meta.getFVarLocalDecl fvar = Lean.Meta.getLocalDecl (Lean.Expr.fvarId! fvar)

source

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

Lean.MetaM Lean.LocalDecl

Equations

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

source

def Lean.Meta.instantiateLevelMVars (u : Lean.Level) :

Lean.MetaM Lean.Level

Equations

Lean.Meta.instantiateLevelMVars u = Lean.MetavarContext.instantiateLevelMVars u

source

def Lean.Meta.instantiateMVars (e : Lean.Expr) :

Lean.MetaM Lean.Expr

Equations

Lean.Meta.instantiateMVars e = Lean.MonadCacheT.run (Lean.MetavarContext.instantiateExprMVars e)

source

def Lean.Meta.instantiateLocalDeclMVars (localDecl : Lean.LocalDecl) :

Lean.MetaM Lean.LocalDecl

Equations

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

source

@[inline]

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

Lean.MetaM α

Equations

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

source

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

Lean.MetaM Lean.Expr

Equations

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

source

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.abstract e xs = Lean.Meta.abstractRange e (Array.size xs) xs

source

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

Lean.MetaM Lean.Expr

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

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

Equations

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

source

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

Lean.MetaM Lean.Expr

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

Equations

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

source

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

Lean.MetaM Lean.Expr

Equations

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

source

def Lean.Meta.mkArrow (d : Lean.Expr) (b : Lean.Expr) :

Lean.MetaM Lean.Expr

Creates the expression d → b

Equations

Lean.Meta.mkArrow d b = do let a ← liftM (Lean.mkFreshUserName `x) pure (Lean.mkForall a Lean.BinderInfo.default d b)

source

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

Lean.MetaM Lean.Expr

fun _ : Unit => a

Equations

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

source

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

Lean.MetaM Lean.Expr

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)

source

@[inline]

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

n α → n α

Equations

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

source

@[inline]

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

n α

Equations

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

source

@[inline]

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

n α

Equations

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

source

@[inline]

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

n α → n α

Equations

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

source

@[inline]

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

n α

Equations

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

source

@[inline]

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

n α

Equations

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

source

@[inline]

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

n α

Equations

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

source

@[inline]

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

n α

Equations

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

source

@[inline]

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

n α

Execute x allowing isDefEq to assign synthetic opaque metavariables.

Equations

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

source

@[inline]

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

n α → n α

Equations

Lean.Meta.savingCache = Lean.Meta.mapMetaM fun {α} => Lean.Meta.savingCacheImpl

source

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

Lean.MetaM (Option Lean.ConstantInfo)

Equations

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

source

def Lean.Meta.saveAndResetSynthInstanceCache:

Lean.MetaM Lean.Meta.SynthInstanceCache

Equations

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

source

def Lean.Meta.restoreSynthInstanceCache (cache : Lean.Meta.SynthInstanceCache) :

Lean.MetaM Unit

Equations

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

source

@[inline]

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

n α → n α

Reset synthInstance cache, execute x, and restore cache

Equations

Lean.Meta.resettingSynthInstanceCache = Lean.Meta.mapMetaM fun {α} => Lean.Meta.resettingSynthInstanceCacheImpl

source

@[inline]

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

n α

Equations

Lean.Meta.resettingSynthInstanceCacheWhen b x = if b = true then Lean.Meta.resettingSynthInstanceCache x else x

source

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

n α → n α

Add entry { className := className, fvar := fvar } to localInstances, and then execute continuation k. It resets the type class cache using resettingSynthInstanceCache.

Equations

Lean.Meta.withNewLocalInstance className fvar = Lean.Meta.mapMetaM fun {α} => Lean.Meta.withNewLocalInstanceImp className fvar

source

def Lean.Meta.isClass? (type : Lean.Expr) :

Lean.MetaM (Option Lean.Name)

Equations

Lean.Meta.isClass? type = tryCatch (Lean.Meta.isClassImp? type) fun x => pure none

source

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

n α → n α

Equations

Lean.Meta.withNewLocalInstances fvars j = Lean.Meta.mapMetaM fun {α} => Lean.Meta.withNewLocalInstancesImpAux fvars j

source

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

n α

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

Equations

Lean.Meta.forallTelescope type k = Lean.Meta.map2MetaM (fun {α} k => Lean.Meta.forallTelescopeImp type k) k

source

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

n α

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

Equations

Lean.Meta.forallTelescopeReducing type k = Lean.Meta.map2MetaM (fun {α} k => Lean.Meta.forallTelescopeReducingImp type k) k

source

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

n α

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

Equations

Lean.Meta.forallBoundedTelescope type maxFVars? k = Lean.Meta.map2MetaM (fun {α} k => Lean.Meta.forallBoundedTelescopeImp type maxFVars? k) k

source

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

n α

Similar to lambdaTelescope but for lambda and let expressions.

Equations

Lean.Meta.lambdaLetTelescope e k = Lean.Meta.map2MetaM (fun {α} k => Lean.Meta.lambdaTelescopeImp e true k) k

source

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

n α

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

Equations

Lean.Meta.lambdaTelescope e k = Lean.Meta.map2MetaM (fun {α} k => Lean.Meta.lambdaTelescopeImp e false k) k

source

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

Lean.MetaM (Array Lean.Name)

Return the parameter names for the given global declaration.

Equations

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

source

def Lean.Meta.forallMetaTelescope (e : Lean.Expr) (kind : optParam Lean.MetavarKind Lean.MetavarKind.natural) :

Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)

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

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

Equations

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

source

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

Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)

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

Equations

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

source

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

Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)

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

Equations

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

source

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

Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)

Similar to forallMetaTelescopeReducingAux but for lambda expressions.

Equations

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

source

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

Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)

source

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

n α

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

Equations

Lean.Meta.withLocalDecl name bi type k = Lean.Meta.map1MetaM (fun {α} k => Lean.Meta.withLocalDeclImp name bi type k) k

source

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

n α

Equations

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

source

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

n α

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

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

Equations

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

source

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

n α

source

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

n α

Equations

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

source

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

n α

Equations

Lean.Meta.withNewBinderInfos bs k = Lean.Meta.mapMetaM (fun {α} k => Lean.Meta.withNewBinderInfosImp bs k) k

source

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

n α

Equations

Lean.Meta.withLetDecl name type val k = Lean.Meta.map1MetaM (fun {α} k => Lean.Meta.withLetDeclImp name type val k) k

source

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

Lean.MetaM α

Equations

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

source

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

n α → n α

Equations

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

source

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

n α → n α

Equations

Lean.Meta.withExistingLocalDecls decls = Lean.Meta.mapMetaM fun {α} => Lean.Meta.withExistingLocalDeclsImp decls

source

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

n α → n α

Save cache and MetavarContext, bump the MetavarContext depth, execute x, and restore saved data.

Metavariable context depths are used to control which metavariables may be assigned in isDefEq. See the docstring of isDefEq for more information.

Equations

Lean.Meta.withNewMCtxDepth = Lean.Meta.mapMetaM fun {α} => Lean.Meta.withNewMCtxDepthImp

source

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

n α → n α

Equations

Lean.Meta.withLCtx lctx localInsts = Lean.Meta.mapMetaM fun {α} => Lean.Meta.withLocalContextImp lctx localInsts

source

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

n α → n α

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

Equations

Lean.Meta.withMVarContext mvarId = Lean.Meta.mapMetaM fun {α} => Lean.Meta.withMVarContextImp mvarId

source

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

n α → n α

Equations

Lean.Meta.withMCtx mctx = Lean.Meta.mapMetaM fun {α} => Lean.Meta.withMCtxImp mctx

source

@[inline]

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

n α → n α

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

Equations

Lean.Meta.approxDefEq = Lean.Meta.mapMetaM fun {α} => Lean.Meta.approxDefEqImp

source

@[inline]

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

n α → n α

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

Equations

Lean.Meta.fullApproxDefEq = Lean.Meta.mapMetaM fun {α} => Lean.Meta.fullApproxDefEqImp

source

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

Lean.MetaM Lean.Level

Equations

Lean.Meta.normalizeLevel u = do let u ← Lean.Meta.instantiateLevelMVars u pure (Lean.Level.normalize u)

source

def Lean.Meta.assignLevelMVar (mvarId : Lean.MVarId) (u : Lean.Level) :

Lean.MetaM Unit

Equations

Lean.Meta.assignLevelMVar mvarId u = Lean.modifyMCtx fun mctx => Lean.MetavarContext.assignLevel mctx mvarId u

source

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

Lean.MetaM Lean.Expr

whnf with reducible transparency.

Equations

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

source

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

Lean.MetaM Lean.Expr

whnf with default transparency.

Equations

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

source

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

Lean.MetaM Lean.Expr

whnf with instances transparency.

Equations

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

source

def Lean.Meta.setInlineAttribute (declName : Lean.Name) (kind : optParam Lean.Compiler.InlineAttributeKind Lean.Compiler.InlineAttributeKind.inline) :

Lean.MetaM Unit

Equations

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

source

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

Lean.MetaM Lean.Expr

Equations

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

source

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

Lean.MetaM Lean.Expr

Equations

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

source

def Lean.Meta.dependsOn (e : Lean.Expr) (fvarId : Lean.FVarId) :

Lean.MetaM Bool

Return true iff e depends on the free variable fvarId

Equations

Lean.Meta.dependsOn e fvarId = do let a ← Lean.getMCtx pure (Lean.MetavarContext.exprDependsOn a e fvarId)

source

def Lean.Meta.localDeclDependsOn (localDecl : Lean.LocalDecl) (fvarId : Lean.FVarId) :

Lean.MetaM Bool

Return true iff e depends on the free variable fvarId

Equations

Lean.Meta.localDeclDependsOn localDecl fvarId = do let a ← Lean.getMCtx pure (Lean.MetavarContext.localDeclDependsOn a localDecl fvarId)

source

def Lean.Meta.dependsOnPred (e : Lean.Expr) (pf : optParam (Lean.FVarId → Bool) fun x => false) (pm : optParam (Lean.MVarId → Bool) fun x => false) :

Lean.MetaM Bool

Return true iff e depends on a free variable x s.t. pf x, or an unassigned metavariable ?m s.t. pm ?m is true.

Equations

Lean.Meta.dependsOnPred e pf pm = do let a ← Lean.getMCtx pure (Lean.MetavarContext.findExprDependsOn a e pf pm)

source

def Lean.Meta.localDeclDependsOnPred (localDecl : Lean.LocalDecl) (pf : optParam (Lean.FVarId → Bool) fun x => false) (pm : optParam (Lean.MVarId → Bool) fun x => false) :

Lean.MetaM Bool

Return true iff the local declaration localDecl depends on a free variable x s.t. pf x, an unassigned metavariable ?m s.t. pm ?m is true.

Equations

Lean.Meta.localDeclDependsOnPred localDecl pf pm = do let a ← Lean.getMCtx pure (Lean.MetavarContext.findLocalDeclDependsOn a localDecl pf pm)

source

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

Lean.MetaM Lean.Format

Equations

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

source

@[inline]

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

Lean.MetaM α

Equations

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

source

instance Lean.Meta.instOrElseMetaM {α : Type} :

OrElse (Lean.MetaM α)

Equations

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

source

instance Lean.Meta.instAlternativeMetaM:

Alternative Lean.MetaM

Equations

Lean.Meta.instAlternativeMetaM = Alternative.mk (fun {x} => Lean.throwError (Lean.toMessageData "failed")) fun {α} => Lean.Meta.orElse

source

@[inline]

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

m α

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

Equations

Lean.Meta.orelseMergeErrors x y mergeRef mergeMsg = controlAt Lean.MetaM fun runInBase => Lean.Meta.orelseMergeErrorsImp (runInBase x) (runInBase y) mergeRef mergeMsg

source

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

Lean.MetaM α

Execute x, and apply f to the produced error message

Equations

Lean.Meta.mapErrorImp x f = tryCatch x fun ex => match ex with | Lean.Exception.error ref msg => throw (Lean.Exception.error ref (f msg)) | ex => throw ex

source

@[inline]

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

m α

Equations

Lean.Meta.mapError x f = controlAt Lean.MetaM fun runInBase => Lean.Meta.mapErrorImp (runInBase x) f

source

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

Lean.MetaM (Array Lean.FVarId)

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

Equations

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

source

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

Lean.MetaM Bool

Equations

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

source

def Lean.Meta.isListLevelDefEqAux:

List Lean.Level → List Lean.Level → Lean.MetaM Bool

Equations

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

source

def Lean.Meta.getResetPostponed:

Lean.MetaM (Std.PersistentArray Lean.Meta.PostponedEntry)

Equations

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

source

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

Lean.MetaM Lean.MessageData

Equations

Lean.Meta.mkLevelStuckErrorMessage entry = Lean.Meta.mkLeveErrorMessageCore "stuck at solving universe constraint" entry

source

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

Lean.MetaM Lean.MessageData

Equations

Lean.Meta.mkLevelErrorMessage entry = Lean.Meta.mkLeveErrorMessageCore "failed to solve universe constraint" entry

source

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

Lean.MetaM Bool

Equations

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

source

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

Lean.MetaM Bool

source

@[specialize]

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

Lean.MetaM Bool

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

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

Equations

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

source

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

Lean.MetaM Bool

Equations

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

source

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

Lean.MetaM Bool

Equations

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

source

@[inline]

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

Lean.MetaM Bool

Determines whether two expressions are definitionally equal to each other.

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

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

Equations