Documentation

Lean.Meta.Basic

This module provides four (mutually dependent) goodies that are needed for building the elaborator and tactic frameworks. 1- Weak head normal form computation with support for metavariables and transparency modes. 2- Definitionally equality checking with support for metavariables (aka unification modulo definitional equality). 3- Type inference. 4- Type class resolution.

They are packed into the MetaM monad.

opaque Lean.Meta.isDefEqStuckExceptionId :

Lean.InternalExceptionId

structure Lean.Meta.Config :

Type

If foApprox is set to true, and some aᵢ is not a free variable, then we use first-order unification

  ?m a_1 ... a_i a_{i+1} ... a_{i+k} =?= f b_1 ... b_k

reduces to

  ?m a_1 ... a_i =?= f
  a_{i+1}        =?= b_1
  ...
  a_{i+k}        =?= b_k

foApprox : Bool

When ctxApprox is set to true, we relax condition 4, by creating an auxiliary metavariable ?n' with a smaller context than ?m'.
ctxApprox : Bool
When quasiPatternApprox is set to true, we ignore condition 2.
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
Controls which definitions and theorems can be unfolded by isDefEq and whnf.
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
Enable/disable the unification hints feature.
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

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 in C
t only contains free variables in C and/or {a₁, ..., aₙ}
For every metavariable ?m'@C' occurring in t, C' is a subprefix of C
?m does not occur in t

Instances For

structure Lean.Meta.ParamInfo :

Type

The binder annotation for the parameter.
binderInfo : Lean.BinderInfo
hasFwdDeps is true if there is another parameter whose type depends on this one.
hasFwdDeps : Bool
backDeps contains the backwards dependencies. That is, the (0-indexed) position of previous parameters that this one depends on.
backDeps : Array Nat
isProp is true if the parameter is always a proposition.
isProp : Bool
isDecInst is true if the parameter's type is of the form Decidable .... This information affects the generation of congruence theorems.
isDecInst : Bool
higherOrderOutParam is true if this parameter is a higher-order output parameter of local instance. Example:
```
getElem :
  {cont : Type u_1} → {idx : Type u_2} → {elem : Type u_3} →
  {dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] →
  (xs : cont) → (i : idx) → dom xs i → elem
```
This flag is true for the parameter dom because it is output parameter of [self : GetElem cont idx elem dom]
higherOrderOutParam : Bool
dependsOnHigherOrderOutParam is true if the type of this parameter depends on the higher-order output parameter of a previous local instance. Example:
```
getElem :
  {cont : Type u_1} → {idx : Type u_2} → {elem : Type u_3} →
  {dom : cont → idx → Prop} → [self : GetElem cont idx elem dom] →
  (xs : cont) → (i : idx) → dom xs i → elem
```
This flag is true for the parameter with type dom xs i since dom is an output parameter of the instance [self : GetElem cont idx elem dom]
dependsOnHigherOrderOutParam : Bool

Function parameter information cache.

Instances For

instance Lean.Meta.instInhabitedParamInfo :

Inhabited Lean.Meta.ParamInfo

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

structure Lean.Meta.FunInfo :

Type

Parameter information cache.
paramInfo : Array Lean.Meta.ParamInfo
resultDeps contains the function result type backwards dependencies. That is, the (0-indexed) position of parameters that the result type depends on.
resultDeps : Array Nat

Function information cache. See ParamInfo.

Instances For

structure Lean.Meta.InfoCacheKey :

Type

The transparency mode used to compute the FunInfo.
transparency : Lean.Meta.TransparencyMode
The function being cached information about. It is quite often an Expr.const.
expr : Lean.Expr
nargs? = some n if the cached information was computed assuming the function has arity n. If nargs? = none, then the cache information consumed the arrow type as much as possible unsing the current transparency setting. X
nargs? : Option Nat

Key for the function information cache.

Instances For

instance Lean.Meta.instInhabitedInfoCacheKey :

Inhabited Lean.Meta.InfoCacheKey

Equations

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

instance Lean.Meta.instBEqInfoCacheKey :

BEq Lean.Meta.InfoCacheKey

Equations

Lean.Meta.instBEqInfoCacheKey = { beq := Lean.Meta.beqInfoCacheKey✝ }

instance Lean.Meta.InfoCacheKey.instHashableInfoCacheKey :

Hashable Lean.Meta.InfoCacheKey

Equations

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

@[inline]

abbrev Lean.Meta.SynthInstanceCache :

Type

Equations

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

@[inline]

abbrev Lean.Meta.InferTypeCache :

Type

Equations

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

@[inline]

abbrev Lean.Meta.FunInfoCache :

Type

Equations

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

@[inline]

abbrev Lean.Meta.WhnfCache :

Type

Equations

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

@[inline]

abbrev Lean.Meta.DefEqCache :

Type

A mapping (s, t) ↦ isDefEq s t. TODO: consider more efficient representations (e.g., a proper set) and caching policies (e.g., imperfect cache). We should also investigate the impact on memory consumption.

Equations

Lean.Meta.DefEqCache = Lean.PersistentHashMap (Lean.Expr × Lean.Expr) Bool

structure Lean.Meta.Cache :

Type

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

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

Instances For

instance Lean.Meta.instInhabitedCache :

Inhabited Lean.Meta.Cache

Equations

Lean.Meta.instInhabitedCache = { default := { inferType := default, funInfo := default, synthInstance := default, whnfDefault := default, whnfAll := default, defEq := default } }

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.

Instances For

structure Lean.Meta.PostponedEntry :

Type

We save the ref at entry creation time. This is used for reporting errors back to the user.
ref : Lean.Syntax
lhs : Lean.Level
rhs : Lean.Level
Context for the surrounding isDefEq call when entry was created.
ctx? : Option Lean.Meta.DefEqContext

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.

Instances For

instance Lean.Meta.instInhabitedPostponedEntry :

Inhabited Lean.Meta.PostponedEntry

Equations

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

structure Lean.Meta.State :

Type

mctx : Lean.MetavarContext
cache : Lean.Meta.Cache
When trackZeta == true, then any let-decl free variable that is zeta expansion performed by MetaM is stored in zetaFVarIds.
zetaFVarIds : Lean.FVarIdSet
Array of postponed universe level constraints
postponed : Lean.PersistentArray Lean.Meta.PostponedEntry

MetaM monad state.

Instances For

instance Lean.Meta.instInhabitedState :

Inhabited Lean.Meta.State

Equations

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

structure Lean.Meta.SavedState :

Type

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

Backtrackable state for the MetaM monad.

Instances For

instance Lean.Meta.instInhabitedSavedState :

Inhabited Lean.Meta.SavedState

Equations

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

structure Lean.Meta.Context :

Type

config : Lean.Meta.Config
Local context
lctx : Lean.LocalContext
Local instances in lctx.
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)

Contextual information for the MetaM monad.

Instances For

@[inline]

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

Type

Equations

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

instance Lean.Meta.instMonadMetaM :

Monad Lean.MetaM

Equations

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

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

Inhabited (Lean.MetaM α)

Equations

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

instance Lean.Meta.instMonadLCtxMetaM :

Lean.MonadLCtx Lean.MetaM

Equations

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

instance Lean.Meta.instMonadMCtxMetaM :

Lean.MonadMCtx Lean.MetaM

Equations

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

instance Lean.Meta.instMonadEnvMetaM :

Lean.MonadEnv Lean.MetaM

Equations

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

instance Lean.Meta.instAddMessageContextMetaM :

Lean.AddMessageContext Lean.MetaM

Equations

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

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 }

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.

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 }

@[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 := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none }) (s : optParam Lean.Meta.State { mctx := { depth := 0, mvarCounter := 0, lDepth := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, cache := { inferType := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, funInfo := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, synthInstance := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfDefault := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfAll := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEq := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, zetaFVarIds := ∅, postponed := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }) :

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

Equations

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

@[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 := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none }) (s : optParam Lean.Meta.State { mctx := { depth := 0, mvarCounter := 0, lDepth := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, cache := { inferType := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, funInfo := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, synthInstance := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfDefault := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfAll := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEq := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, zetaFVarIds := ∅, postponed := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }) :

Equations

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

@[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 := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }, localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none }) (s : optParam Lean.Meta.State { mctx := { depth := 0, mvarCounter := 0, lDepth := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, decls := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, userNames := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, lAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, eAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, dAssignment := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, cache := { inferType := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, funInfo := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, synthInstance := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfDefault := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfAll := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, defEq := { root := Lean.PersistentHashMap.Node.entries Lean.PersistentHashMap.mkEmptyEntriesArray, size := 0 } }, zetaFVarIds := ∅, postponed := { root := Lean.PersistentArrayNode.node (Array.mkEmpty (USize.toNat Lean.PersistentArray.branching)), tail := Array.mkEmpty (USize.toNat Lean.PersistentArray.branching), size := 0, shift := Lean.PersistentArray.initShift, tailOff := 0 } }) :

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

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)

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.

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

Equations

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

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

@[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)

@[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)

@[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)

@[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.

@[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.

@[inline]

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

Lean.MetaM Unit

Equations

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

def Lean.Meta.getLocalInstances :

Lean.MetaM Lean.LocalInstances

Equations

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

def Lean.Meta.getConfig :

Lean.MetaM Lean.Meta.Config

Equations

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

def Lean.Meta.resetZetaFVarIds :

Lean.MetaM Unit

Equations

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

def Lean.Meta.getZetaFVarIds :

Lean.MetaM Lean.FVarIdSet

Equations

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

def Lean.Meta.getPostponed :

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

Return the array of postponed universe level constraints.

Equations

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

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

Lean.MetaM Unit

Set the array of postponed universe level constraints.

Equations

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

@[inline]

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

Lean.MetaM Unit

Modify the array of postponed universe level constraints.

Equations

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

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

Lean.MetaM Bool

useEtaStruct inductName return true if we eta for structures is enabled for for the inductive datatype inductName.

Recall we have three different settings: .none (never use it), .all (always use it), .notClasses (enabled only for structure-like inductive types that are not classes).

The parameter inductName affects the result only if the current setting is .notClasses.

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.

@[extern 6 lean_whnf]

opaque Lean.Meta.whnf :

Lean.Expr → Lean.MetaM Lean.Expr

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

@[extern 6 lean_infer_type]

opaque Lean.Meta.inferType :

Lean.Expr → Lean.MetaM Lean.Expr

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

@[extern 7 lean_is_expr_def_eq]

opaque Lean.Meta.isExprDefEqAux :

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

@[extern 7 lean_is_level_def_eq]

opaque Lean.Meta.isLevelDefEqAux :

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

@[extern 6 lean_synth_pending]

opaque Lean.Meta.synthPending :

Lean.MVarId → Lean.MetaM Bool

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

Lean.MetaM Lean.Expr

Equations

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

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

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

def Lean.Meta.mkFreshLevelMVar :

Lean.MetaM Lean.Level

Equations

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

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

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

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.

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

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

Lean.MetaM (List Lean.Level)

Equations

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

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

Lean.MetaM Lean.Expr

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 a ← Lean.Meta.mkFreshLevelMVarsFor info pure (Lean.mkConst declName a)

def Lean.Meta.getTransparency :

Lean.MetaM Lean.Meta.TransparencyMode

Return current transparency setting/mode.

Equations

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

def Lean.Meta.shouldReduceAll :

Lean.MetaM Bool

Equations

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

def Lean.Meta.shouldReduceReducibleOnly :

Lean.MetaM Bool

Equations

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

def Lean.MVarId.findDecl? (mvarId : Lean.MVarId) :

Lean.MetaM (Option Lean.MetavarDecl)

Return some mvarDecl where mvarDecl is mvarId declaration in the current metavariable context. Return none if mvarId has no declaration in the current metavariable context.

Equations

Lean.MVarId.findDecl? mvarId = do let a ← Lean.getMCtx pure (Lean.MetavarContext.findDecl? a mvarId)

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

Lean.MetaM (Option Lean.MetavarDecl)

Equations

Lean.Meta.findMVarDecl? mvarId = Lean.MVarId.findDecl? mvarId

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

Lean.MetaM Lean.MetavarDecl

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

Equations

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

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

Lean.MetaM Lean.MetavarDecl

Equations

Lean.Meta.getMVarDecl mvarId = Lean.MVarId.getDecl mvarId

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

Lean.MetaM Lean.MetavarKind

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

Equations

Lean.MVarId.getKind mvarId = do let a ← Lean.MVarId.getDecl mvarId pure a.kind

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

Lean.MetaM Lean.MetavarKind

Equations

Lean.Meta.getMVarDeclKind mvarId = Lean.MVarId.getKind mvarId

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

Lean.MetaM Bool

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

Equations

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

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

Lean.MetaM Unit

Set mvarId kind in the current metavariable context.

Equations

Lean.MVarId.setKind mvarId kind = Lean.modifyMCtx fun mctx => Lean.MetavarContext.setMVarKind mctx mvarId kind

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

Lean.MetaM Unit

Equations

Lean.Meta.setMVarKind mvarId kind = Lean.MVarId.setKind mvarId kind

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

Lean.MetaM Unit

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

Equations

Lean.MVarId.setType mvarId type = Lean.modifyMCtx fun mctx => Lean.MetavarContext.setMVarType mctx mvarId type

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

Lean.MetaM Unit

Equations

Lean.Meta.setMVarType mvarId type = Lean.MVarId.setType mvarId type

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

Lean.MetaM Bool

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

Equations

Lean.MVarId.isReadOnly mvarId = do let a ← Lean.MVarId.getDecl mvarId let a_1 ← Lean.getMCtx pure (a.depth != a_1.depth)

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

Lean.MetaM Bool

Equations

Lean.Meta.isReadOnlyExprMVar mvarId = Lean.MVarId.isReadOnly mvarId

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

Lean.MetaM Bool

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

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

Equations

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

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

Lean.MetaM Bool

Equations

Lean.Meta.isReadOnlyOrSyntheticOpaqueExprMVar mvarId = Lean.MVarId.isReadOnlyOrSyntheticOpaque mvarId

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

Return the level of the given universe level metavariable.

Equations

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

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

Equations

Lean.Meta.getLevelMVarDepth mvarId = Lean.LMVarId.getLevel mvarId

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

Lean.MetaM Bool

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

Equations

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

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

Lean.MetaM Bool

Equations

Lean.Meta.isReadOnlyLevelMVar mvarId = Lean.LMVarId.isReadOnly mvarId

def Lean.MVarId.setUserName (mvarId : Lean.MVarId) (newUserName : Lean.Name) :

Lean.MetaM Unit

Set the user-facing name for the given metavariable.

Equations

Lean.MVarId.setUserName mvarId newUserName = Lean.modifyMCtx fun mctx => Lean.MetavarContext.setMVarUserName mctx mvarId newUserName

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

Lean.MetaM Unit

Equations

Lean.Meta.setMVarUserName mvarId userNameNew = Lean.MVarId.setUserName mvarId userNameNew

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

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 "'")

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

Equations

Lean.Meta.throwUnknownFVar fvarId = liftM (Lean.FVarId.throwUnknown fvarId)

def Lean.FVarId.findDecl? (fvarId : Lean.FVarId) :

Lean.MetaM (Option Lean.LocalDecl)

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

Equations

Lean.FVarId.findDecl? fvarId = do let a ← Lean.getLCtx pure (Lean.LocalContext.find? a fvarId)

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

Lean.MetaM (Option Lean.LocalDecl)

Equations

Lean.Meta.findLocalDecl? fvarId = Lean.FVarId.findDecl? fvarId

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

Lean.MetaM Lean.LocalDecl

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

Equations

Lean.FVarId.getDecl fvarId = do let a ← Lean.getLCtx match Lean.LocalContext.find? a fvarId with | some d => pure d | none => liftM (Lean.FVarId.throwUnknown fvarId)

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

Lean.MetaM Lean.LocalDecl

Equations

Lean.Meta.getLocalDecl fvarId = Lean.FVarId.getDecl fvarId

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

Lean.MetaM Lean.Expr

Return the type of the given free variable.

Equations

Lean.FVarId.getType fvarId = do let a ← Lean.FVarId.getDecl fvarId pure (Lean.LocalDecl.type a)

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

Lean.MetaM Lean.BinderInfo

Return the binder information for the given free variable.

Equations

Lean.FVarId.getBinderInfo fvarId = do let a ← Lean.FVarId.getDecl fvarId pure (Lean.LocalDecl.binderInfo a)

def Lean.FVarId.getValue? (fvarId : Lean.FVarId) :

Lean.MetaM (Option Lean.Expr)

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

Equations

Lean.FVarId.getValue? fvarId = do let a ← Lean.FVarId.getDecl fvarId pure (Lean.LocalDecl.value? a)

def Lean.FVarId.getUserName (fvarId : Lean.FVarId) :

Lean.MetaM Lean.Name

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

Equations

Lean.FVarId.getUserName fvarId = do let a ← Lean.FVarId.getDecl fvarId pure (Lean.LocalDecl.userName a)

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

Lean.MetaM Bool

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

Equations

Lean.FVarId.isLetVar fvarId = do let a ← Lean.FVarId.getDecl fvarId pure (Lean.LocalDecl.isLet a)

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

Lean.MetaM Lean.LocalDecl

Get the local declaration associated to the given Expr in the current local context. Fails if the given expression is not a fvar or if no such declaration exists.

Equations

Lean.Meta.getFVarLocalDecl fvar = Lean.FVarId.getDecl (Lean.Expr.fvarId! fvar)

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

Lean.MetaM Lean.LocalDecl

Given a user-facing name for a free variable, return its declaration in the current local context. Throw an exception if free variable is not declared.

Equations

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

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

Lean.MetaM Lean.Expr

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

@[inline]

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

Lift a MkBindingM monadic action x to MetaM.

Equations

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

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

Lean.MetaM Lean.Expr

Similar to abstracM but consider only the first min n xs.size entries in xs

It is also similar to Expr.abstractRange, but handles metavariables correctly. It uses elimMVarDeps to ensure e and the type of the free variables xs do not contain a metavariable ?m s.t. local context of ?m contains a free variable in xs.

Equations

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

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.Expr.abstractRangeM e n xs

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

Lean.MetaM Lean.Expr

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

Equations

Lean.Expr.abstractM e xs = Lean.Expr.abstractRangeM e (Array.size xs) xs

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.abstract e xs = Lean.Expr.abstractM e xs

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

Lean.MetaM (Array Lean.Expr)

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

Equations

Lean.Meta.collectForwardDeps toRevert preserveOrder = Lean.Meta.liftMkBindingM (Lean.MetavarContext.collectForwardDeps toRevert preserveOrder)

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.

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.

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

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 (Lean.Name.mkStr1 "x")) pure (Lean.mkLambda a Lean.BinderInfo.default (Lean.mkConst (Lean.Name.mkStr1 "Unit")) a)

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)

@[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 α

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.

@[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.

@[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.

@[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.

@[inline]

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

n α

withDefault x excutes x using the default transparency setting.

Equations

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

@[inline]

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

n α

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

Equations

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

@[inline]

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

n α

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

Equations

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

@[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 α

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.

@[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.

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

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

def Lean.Meta.saveAndResetSynthInstanceCache :

Lean.MetaM Lean.Meta.SynthInstanceCache

Equations

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

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

Lean.MetaM Unit

Equations

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

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

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

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

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

Lean.MetaM (Option Lean.Name)

isClass? type return some ClsName if type is an instance of the class ClsName. Example:

#eval do
  let x ← mkAppM ``Inhabited #[mkConst ``Nat]
  IO.println (← isClass? x)
  -- (some Inhabited)

Equations

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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 #[]

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 α

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.

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

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

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

Equations

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

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 α

Add the local declaration : := to the local context and execute k x, where x is a new free variable corresponding to the let-declaration. After executing k x, the local context is restored.

Equations

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

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

Equations

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

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

n α → n α

Register any local instance in decls

Equations

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

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

n α → n α

withExistingLocalDecls decls k, adds the given local declarations to the local context, and then executes k. This method assumes declarations in decls have valid FVarIds. After executing k, the local context is restored.

Remark: this method is used, for example, to implement the match-compiler. Each match-alternative commes with a local declarations (corresponding to pattern variables), and we use withExistingLocalDecls to add them to the local context before we process them.

Equations

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

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

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 α

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 {α} => Lean.Meta.withLocalContextImp lctx localInsts

def Lean.MVarId.withContext {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.MVarId.withContext mvarId = Lean.Meta.mapMetaM fun {α} => Lean.Meta.withMVarContextImp mvarId

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

n α → n α

Equations

Lean.Meta.withMVarContext mvarId = Lean.MVarId.withContext mvarId

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

n α → n α

withMCtx mctx k replaces the metavariable context and then executes k. The metavariable context is restored after executing k.

This method is used to implement the type class resolution procedure.

Equations

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

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

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

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

Lean.MetaM Lean.Level

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)

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)

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)

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)

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

Lean.MetaM Unit

Mark declaration declName with the attribute [inline]. This method does not check whether the given declaration is a definition.

Recall that this attribute can only be set in the same module where declName has been declared.

Equations

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

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

Lean.MetaM Lean.Expr

Given e of the form forall (a_1 : A_1) ... (a_n : A_n), B[a_1, ..., a_n] and p_1 : A_1, ... p_n : A_n, return B[p_1, ..., p_n].

Equations

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

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

Lean.MetaM Lean.Expr

Given e of the form fun (a_1 : A_1) ... (a_n : A_n) => t[a_1, ..., a_n] and p_1 : A_1, ... p_n : A_n, return t[p_1, ..., p_n]. It uses whnf to reduce e if it is not a lambda

Equations

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

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

Lean.MetaM Lean.Format

Pretty-print the given expression.

Equations

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

@[inline]

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

Equations

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

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

OrElse (Lean.MetaM α)

Equations

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

instance Lean.Meta.instAlternativeMetaM :

Alternative Lean.MetaM

Equations

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

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

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

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

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

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.

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

Lean.MetaM Bool

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.

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

def Lean.Meta.getNumPostponed :

Equations

Lean.Meta.getNumPostponed = do let a ← Lean.Meta.getPostponed pure a.size

def Lean.Meta.getResetPostponed :

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

Equations

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

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

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

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.

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

Lean.MetaM Bool

@[specialize #[]]

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

Lean.MetaM Bool

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

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

Equations

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

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

Lean.MetaM Bool

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

Equations

Lean.Meta.isLevelDefEq u v = Lean.Meta.checkpointDefEq (Lean.Meta.isLevelDefEqAux u v) true

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

Lean.MetaM Bool

See isDefEq.

Equations

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

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

Lean.Meta.isDefEq t s = Lean.Meta.isExprDefEq t s

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

Lean.MetaM Bool

Equations

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

@[inline]

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

Lean.MetaM Bool

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

Equations

Lean.Meta.isDefEqGuarded t s = Lean.Meta.isExprDefEqGuarded t s

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

Lean.MetaM Bool

Equations

Lean.Meta.isDefEqNoConstantApprox t s = Lean.Meta.approxDefEq (Lean.Meta.isDefEq t s)

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

Lean.MetaM Lean.Expr

Eta expand the given expression. Example:

etaExpand (mkConst ``Nat.add)

produces fun x y => Nat.add x y

Equations

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