Lean.Meta.Basic

Lean.Meta.InfoCacheKey.instHashableInfoCacheKey = { hash := fun x => match x with | { transparency := transparency, expr := expr, nargs? := nargs } => mixHash (hash transparency) (mixHash (hash expr) (hash nargs)) }

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

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

source

structure Lean.Meta.DefEqContext :

Type

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

source

structure Lean.Meta.PostponedEntry :

Type

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
defEqCtx? : Option Lean.Meta.DefEqContext
synthPendingDepth : Nat
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

Lean.Meta.instMonadMCtxMetaM = { getMCtx := do let a ← get pure a.mctx, modifyMCtx := fun f => modify fun s => { mctx := f s.mctx, cache := s.cache, zetaFVarIds := s.zetaFVarIds, postponed := s.postponed } }

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

Equations

Lean.Meta.SavedState.restore b = do liftM (Lean.Core.restore b.core) modify fun s => { mctx := b.meta.mctx, cache := s.cache, zetaFVarIds := b.meta.zetaFVarIds, postponed := b.meta.postponed }

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 := true }, 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 := true }, 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 := true }, 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 let x : (α × Lean.Meta.State) × Lean.Core.State := discr match x with | ((a, s), sCore) => pure (a, sCore, s)

source

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

Lean.MetaEval (Lean.MetaM α)

Equations

Lean.Meta.instMetaEvalMetaM = { eval := fun env opts x x_1 => Lean.MetaEval.eval env opts (Lean.Meta.MetaM.run' x { 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 := true }, 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 } { 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 } }) true }

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

Lean.Meta.modifyCache f = modify fun x => match x with | { mctx := mctx, cache := cache, zetaFVarIds := zetaFVarIds, postponed := postponed } => { mctx := mctx, cache := f cache, zetaFVarIds := zetaFVarIds, postponed := postponed }

source

@[inline]

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

Lean.MetaM Unit

Equations

Lean.Meta.modifyInferTypeCache f = Lean.Meta.modifyCache fun x => match x with | { inferType := ic, funInfo := c1, synthInstance := c2, whnfDefault := c3, whnfAll := c4, defEqDefault := c5, defEqAll := c6 } => { inferType := f ic, funInfo := c1, synthInstance := c2, whnfDefault := c3, whnfAll := c4, defEqDefault := c5, defEqAll := c6 }

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

@[extern 6lean_whnf]

constant Lean.Meta.whnf :

Lean.Expr → Lean.MetaM Lean.Expr

source

@[extern 6lean_infer_type]

constant Lean.Meta.inferType :

Lean.Expr → Lean.MetaM Lean.Expr

source

@[extern 7lean_is_expr_def_eq]

constant Lean.Meta.isExprDefEqAux :

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

source

@[extern 7lean_is_level_def_eq]

constant Lean.Meta.isLevelDefEqAux :

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

source

@[extern 6lean_synth_pending]

constant 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

Lean.Meta.mkFreshExprMVarWithId mvarId type? kind userName = match type? with | some type => Lean.Meta.mkFreshExprMVarWithIdCore mvarId type kind userName 0 | none => do let u ← Lean.Meta.mkFreshLevelMVar let type ← Lean.Meta.mkFreshExprMVar (some (Lean.mkSort u)) Lean.MetavarKind.natural Lean.Name.anonymous Lean.Meta.mkFreshExprMVarWithIdCore mvarId type kind userName 0

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

Lean.Meta.getMVarDecl mvarId = do let a ← Lean.getMCtx match Lean.MetavarContext.findDecl? a mvarId with | some d => pure d | none => Lean.throwError (Lean.toMessageData "unknown metavariable '?" ++ Lean.toMessageData mvarId.name ++ Lean.toMessageData "'")

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

Lean.Meta.isReadOnlyOrSyntheticOpaqueExprMVar mvarId = do let mvarDecl ← Lean.Meta.getMVarDecl mvarId match mvarDecl.kind with | Lean.MetavarKind.syntheticOpaque => do let a ← Lean.Meta.getConfig pure !a.assignSyntheticOpaque | x => do let a ← Lean.getMCtx pure (mvarDecl.depth != a.depth)

source

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

Lean.MetaM Nat

Equations

Lean.Meta.getLevelMVarDepth mvarId = do let a ← Lean.getMCtx match Lean.MetavarContext.findLevelDepth? a mvarId with | some depth => pure depth | x => Lean.throwError (Lean.toMessageData "unknown universe metavariable '?" ++ Lean.toMessageData mvarId.name ++ Lean.toMessageData "'")

source

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

Lean.MetaM Bool

Equations

Lean.Meta.isReadOnlyLevelMVar mvarId = do let a ← Lean.Meta.getConfig if a.ignoreLevelMVarDepth = true then pure false else do let a ← Lean.Meta.getLevelMVarDepth mvarId let a_1 ← Lean.getMCtx pure (a != a_1.depth)

source

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

Lean.MetaM Unit

Equations

Lean.Meta.renameMVar mvarId newUserName = Lean.modifyMCtx fun mctx => Lean.MetavarContext.renameMVar 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

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

Lean.Meta.getLocalDeclFromUserName userName = do let a ← Lean.getLCtx match Lean.LocalContext.findFromUserName? a userName with | some d => pure d | none => Lean.throwError (Lean.toMessageData "unknown local declaration '" ++ Lean.toMessageData userName ++ Lean.toMessageData "'")

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

Lean.Meta.instantiateLocalDeclMVars localDecl = match localDecl with | Lean.LocalDecl.cdecl idx id n type bi => do let a ← Lean.Meta.instantiateMVars type pure (Lean.LocalDecl.cdecl idx id n a bi) | Lean.LocalDecl.ldecl idx id n type val nonDep => do let a ← Lean.Meta.instantiateMVars type let a_1 ← Lean.Meta.instantiateMVars val pure (Lean.LocalDecl.ldecl idx id n a a_1 nonDep)

source

@[inline]

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

Lean.MetaM α

Equations

Lean.Meta.liftMkBindingM x = do let a ← Lean.getLCtx let a_1 ← Lean.getMCtx let a_2 ← Lean.getNGen match x a { mctx := a_1, ngen := a_2, cache := ∅ } with | EStateM.Result.ok e newS => do Lean.setNGen newS.ngen Lean.Meta.setMCtx newS.mctx pure e | EStateM.Result.error (Lean.MetavarContext.MkBinding.Exception.revertFailure mctx lctx toRevert decl) newS => do Lean.Meta.setMCtx newS.mctx Lean.setNGen newS.ngen Lean.throwError (Lean.toMessageData "failed to create binder due to failure when reverting variable dependencies")

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkForallFVars xs e usedOnly usedLetOnly = if Array.isEmpty xs = true then pure e else Lean.Meta.liftMkBindingM (Lean.MetavarContext.mkForall xs e usedOnly usedLetOnly)

source

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

Lean.MetaM Lean.Expr

Equations

Lean.Meta.mkLambdaFVars xs e usedOnly usedLetOnly = if Array.isEmpty xs = true then pure e else Lean.Meta.liftMkBindingM (Lean.MetavarContext.mkLambda xs e usedOnly usedLetOnly)

source

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

Lean.MetaM Lean.Expr

Equations

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

source

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

Lean.MetaM Lean.Expr

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

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

Lean.Meta.withConfig f = Lean.Meta.mapMetaM fun {α} => withReader fun ctx => { config := f ctx.config, lctx := ctx.lctx, localInstances := ctx.localInstances, defEqCtx? := ctx.defEqCtx?, synthPendingDepth := ctx.synthPendingDepth, canUnfold? := ctx.canUnfold? }

source

@[inline]

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

n α

Equations

Lean.Meta.withTrackingZeta x = Lean.Meta.withConfig (fun cfg => { foApprox := cfg.foApprox, ctxApprox := cfg.ctxApprox, quasiPatternApprox := cfg.quasiPatternApprox, constApprox := cfg.constApprox, isDefEqStuckEx := cfg.isDefEqStuckEx, transparency := cfg.transparency, zetaNonDep := cfg.zetaNonDep, trackZeta := true, unificationHints := cfg.unificationHints, proofIrrelevance := cfg.proofIrrelevance, assignSyntheticOpaque := cfg.assignSyntheticOpaque, ignoreLevelMVarDepth := cfg.ignoreLevelMVarDepth, offsetCnstrs := cfg.offsetCnstrs, etaStruct := cfg.etaStruct }) x

source

@[inline]

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

n α

Equations

Lean.Meta.withoutProofIrrelevance x = Lean.Meta.withConfig (fun cfg => { foApprox := cfg.foApprox, ctxApprox := cfg.ctxApprox, quasiPatternApprox := cfg.quasiPatternApprox, constApprox := cfg.constApprox, isDefEqStuckEx := cfg.isDefEqStuckEx, transparency := cfg.transparency, zetaNonDep := cfg.zetaNonDep, trackZeta := cfg.trackZeta, unificationHints := cfg.unificationHints, proofIrrelevance := false, assignSyntheticOpaque := cfg.assignSyntheticOpaque, ignoreLevelMVarDepth := cfg.ignoreLevelMVarDepth, offsetCnstrs := cfg.offsetCnstrs, etaStruct := cfg.etaStruct }) x

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

Lean.Meta.withTransparency mode = Lean.Meta.mapMetaM fun {α} => Lean.Meta.withConfig fun config => { foApprox := config.foApprox, ctxApprox := config.ctxApprox, quasiPatternApprox := config.quasiPatternApprox, constApprox := config.constApprox, isDefEqStuckEx := config.isDefEqStuckEx, transparency := mode, zetaNonDep := config.zetaNonDep, trackZeta := config.trackZeta, unificationHints := config.unificationHints, proofIrrelevance := config.proofIrrelevance, assignSyntheticOpaque := config.assignSyntheticOpaque, ignoreLevelMVarDepth := config.ignoreLevelMVarDepth, offsetCnstrs := config.offsetCnstrs, etaStruct := config.etaStruct }

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

Lean.Meta.withAtLeastTransparency mode x = Lean.Meta.withConfig (fun config => let oldMode := config.transparency; let mode := if Lean.Meta.TransparencyMode.lt oldMode mode = true then mode else oldMode; { foApprox := config.foApprox, ctxApprox := config.ctxApprox, quasiPatternApprox := config.quasiPatternApprox, constApprox := config.constApprox, isDefEqStuckEx := config.isDefEqStuckEx, transparency := mode, zetaNonDep := config.zetaNonDep, trackZeta := config.trackZeta, unificationHints := config.unificationHints, proofIrrelevance := config.proofIrrelevance, assignSyntheticOpaque := config.assignSyntheticOpaque, ignoreLevelMVarDepth := config.ignoreLevelMVarDepth, offsetCnstrs := config.offsetCnstrs, etaStruct := config.etaStruct }) x

source

@[inline]

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

n α

Equations

Lean.Meta.withAssignableSyntheticOpaque x = Lean.Meta.withConfig (fun config => { foApprox := config.foApprox, ctxApprox := config.ctxApprox, quasiPatternApprox := config.quasiPatternApprox, constApprox := config.constApprox, isDefEqStuckEx := config.isDefEqStuckEx, transparency := config.transparency, zetaNonDep := config.zetaNonDep, trackZeta := config.trackZeta, unificationHints := config.unificationHints, proofIrrelevance := config.proofIrrelevance, assignSyntheticOpaque := true, ignoreLevelMVarDepth := config.ignoreLevelMVarDepth, offsetCnstrs := config.offsetCnstrs, etaStruct := config.etaStruct }) x

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

Lean.Meta.saveAndResetSynthInstanceCache = do let a ← get let savedSythInstance : Lean.Meta.SynthInstanceCache := a.cache.synthInstance Lean.Meta.modifyCache fun c => { inferType := c.inferType, funInfo := c.funInfo, synthInstance := { root := Std.PersistentHashMap.Node.entries Std.PersistentHashMap.mkEmptyEntriesArray, size := 0 }, whnfDefault := c.whnfDefault, whnfAll := c.whnfAll, defEqDefault := c.defEqDefault, defEqAll := c.defEqAll } pure savedSythInstance

source

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

Lean.MetaM Unit

Equations

Lean.Meta.restoreSynthInstanceCache cache = Lean.Meta.modifyCache fun c => { inferType := c.inferType, funInfo := c.funInfo, synthInstance := cache, whnfDefault := c.whnfDefault, whnfAll := c.whnfAll, defEqDefault := c.defEqDefault, defEqAll := c.defEqAll }

source

@[inline]

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

n α → n α

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 α

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 α

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 α

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 α

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} (type : Lean.Expr) (k : Array Lean.Expr → Lean.Expr → n α) :

n α

Equations

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

source

def Lean.Meta.lambdaTelescope {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 α

Equations

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

source

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

Lean.MetaM (Array Lean.Name)

Equations

Lean.Meta.getParamNames declName = do let a ← Lean.getConstInfo declName Lean.Meta.forallTelescopeReducing (Lean.ConstantInfo.type a) fun xs x => Array.mapM (fun x => do let localDecl ← Lean.Meta.getLocalDecl (Lean.Expr.fvarId! x) pure (Lean.LocalDecl.userName localDecl)) xs

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)

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)

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)

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)

Equations

Lean.Meta.lambdaMetaTelescope e maxMVars? = (fun process => process #[] #[] 0 e) (Lean.Meta.lambdaMetaTelescope.process maxMVars?)

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 α

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 α

Equations

Lean.Meta.withLocalDecls declInfos k = (fun loop => loop inst #[]) (@Lean.Meta.withLocalDecls.loop n inst inst α 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

Lean.Meta.withLocalDeclsD declInfos k = Lean.Meta.withLocalDecls (Array.map (fun x => match x with | (name, typeCtor) => (name, Lean.BinderInfo.default, typeCtor)) declInfos) k

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

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 α

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 α

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 α

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

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

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

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

Lean.Meta.setInlineAttribute declName kind = do let env ← Lean.getEnv match Lean.Compiler.setInlineAttribute env declName kind with | Except.ok env => Lean.setEnv env | Except.error msg => Lean.throwError (Function.comp Lean.MessageData.ofFormat Lean.format msg)

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

Equations

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

source

def Lean.Meta.dependsOnPred (e : Lean.Expr) (p : Lean.FVarId → Bool) :

Lean.MetaM Bool

Equations

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

source

def Lean.Meta.localDeclDependsOnPred (localDecl : Lean.LocalDecl) (p : Lean.FVarId → Bool) :

Lean.MetaM Bool

Equations

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

source

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

Lean.MetaM Lean.Format

Equations

Lean.Meta.ppExpr e = do let ctxCore ← readThe Lean.Core.Context let a ← Lean.getEnv let a_1 ← Lean.getMCtx let a_2 ← Lean.getLCtx let a_3 ← Lean.getOptions liftM (Lean.ppExpr { env := a, mctx := a_1, lctx := a_2, opts := a_3, currNamespace := ctxCore.currNamespace, openDecls := ctxCore.openDecls } e)

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 {α} => 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₁ r₂ => 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 α

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 α

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)

Equations

Lean.Meta.sortFVarIds fvarIds = do let lctx ← Lean.getLCtx pure (Array.qsort fvarIds (fun fvarId₁ fvarId₂ => let _discr := Lean.LocalContext.find? lctx fvarId₂; match Lean.LocalContext.find? lctx fvarId₁, Lean.LocalContext.find? lctx fvarId₂ with | some d₁, some d₂ => decide (Lean.LocalDecl.index d₁ < Lean.LocalDecl.index d₂) | some x, none => false | none, some x => true | none, none => Lean.Name.quickLt fvarId₁.name fvarId₂.name) 0 (Array.size fvarIds - 1))

source

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

Lean.MetaM Bool

Equations

Lean.Meta.isInductivePredicate declName = do let a ← Lean.getEnv match Lean.Environment.find? a declName with | some (Lean.ConstantInfo.inductInfo { toConstantVal := { name := x, levelParams := x_1, type := type }, numParams := x_2, numIndices := x_3, all := x_4, ctors := x_5, isRec := x_6, isUnsafe := x_7, isReflexive := x_8, isNested := x_9 }) => Lean.Meta.forallTelescopeReducing type fun x type => do let a ← Lean.Meta.whnfD type match a with | Lean.Expr.sort u x => pure (u == Lean.levelZero) | x => pure false | x => pure false

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 x x = pure false

source

def Lean.Meta.getResetPostponed :

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

Equations

Lean.Meta.getResetPostponed = do let ps ← Lean.Meta.getPostponed Lean.Meta.setPostponed { 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 } pure ps

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

Lean.Meta.processPostponed mayPostpone exceptionOnFailure = do let a ← Lean.Meta.getNumPostponed if (a == 0) = true then pure true else Lean.traceCtx `Meta.isLevelDefEq.postponed ((fun loop => loop) (Lean.Meta.processPostponed.loop mayPostpone exceptionOnFailure))

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

Equations

Lean.Meta.checkpointDefEq x mayPostpone = do let s ← Lean.saveState let postponed ← Lean.Meta.getResetPostponed let r ← tryCatch (do let a ← x if a = true then do let a ← Lean.Meta.processPostponed mayPostpone false if a = true then do let newPostponed ← Lean.Meta.getPostponed Lean.Meta.setPostponed (postponed ++ newPostponed) pure (DoResultPR.return true PUnit.unit) else do Lean.Meta.SavedState.restore s pure (DoResultPR.return false PUnit.unit) else do Lean.Meta.SavedState.restore s pure (DoResultPR.return false PUnit.unit)) fun ex => do Lean.Meta.SavedState.restore s let y ← throw ex pure (DoResultPR.pure y PUnit.unit) match r with | DoResultPR.pure a u => let x := u; pure a | DoResultPR.return b u => let x := u; pure b

source

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

Lean.MetaM Bool

Equations

Lean.Meta.isLevelDefEq u v = Lean.traceCtx `Meta.isLevelDefEq do let b ← Lean.Meta.checkpointDefEq (Lean.Meta.isLevelDefEqAux u v) true let cls : Lean.Name := `Meta.isLevelDefEq let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Bool := fun y => pure b if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData u ++ Lean.toMessageData " =?= " ++ Lean.toMessageData v ++ Lean.toMessageData " ... " ++ Lean.toMessageData (if b = true then "success" else "failure") ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

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

Lean.MetaM Bool

Equations

Lean.Meta.isExprDefEq t s = Lean.traceCtx `Meta.isDefEq (withReader (fun ctx => { config := ctx.config, lctx := ctx.lctx, localInstances := ctx.localInstances, defEqCtx? := some { lhs := t, rhs := s, lctx := ctx.lctx, localInstances := ctx.localInstances }, synthPendingDepth := ctx.synthPendingDepth, canUnfold? := ctx.canUnfold? }) do let b ← Lean.Meta.checkpointDefEq (Lean.Meta.isExprDefEqAux t s) true let cls : Lean.Name := `Meta.isDefEq let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.MetaM Bool := fun y => pure b if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "" ++ Lean.toMessageData t ++ Lean.toMessageData " =?= " ++ Lean.toMessageData s ++ Lean.toMessageData " ... " ++ Lean.toMessageData (if b = true then "success" else "failure") ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y)