structure Auto.MetaState.Stateextends Lean.Meta.State, Lean.Meta.Context : Type

• mctx : MetavarContext
• cache : Cache
• zetaDeltaFVarIds : FVarIdSet
• postponed : PersistentArray PostponedEntry
• diag : Diagnostics
• config : Lean.Meta.Config
• configKey : UInt64
• trackZetaDelta : Bool
• zetaDeltaSet : FVarIdSet
• lctx : LocalContext
• localInstances : LocalInstances
• defEqCtx? : Option DefEqContext
• synthPendingDepth : Nat
• canUnfold? : Option (Config → ConstantInfo → CoreM Bool)
• univApprox : Bool
• inTypeClassResolution : Bool

structure Auto.MetaState.SavedState : Type

• core : Lean.Core.State
• meta : State

@[reducible, inline]

abbrev Auto.MetaState.MetaStateM (α : Type) : Type

Equations

• Auto.MetaState.MetaStateM = StateRefT' IO.RealWorld Auto.MetaState.State Lean.CoreM

@[always_inline]

instance Auto.MetaState.instMonadMetaStateM : Monad MetaStateM

Equations

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

instance Auto.MetaState.instMonadLCtxMetaStateM : Lean.MonadLCtx MetaStateM

Equations

• Auto.MetaState.instMonadLCtxMetaStateM = { getLCtx := do let __do_lift ← get pure __do_lift.lctx }

instance Auto.MetaState.instMonadMCtxMetaStateM : Lean.MonadMCtx MetaStateM

Equations

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

instance Auto.MetaState.instMonadEnvMetaStateM : Lean.MonadEnv MetaStateM

Equations

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

instance Auto.MetaState.instAddMessageContextMetaStateM : Lean.AddMessageContext MetaStateM

Equations

• Auto.MetaState.instAddMessageContextMetaStateM = { addMessageContext := Lean.addMessageContextFull }

def Auto.MetaState.saveState : MetaStateM SavedState

Equations

• Auto.MetaState.saveState = do let __do_lift ← getThe Lean.Core.State let __do_lift_1 ← get pure { core := __do_lift, meta := __do_lift_1 }

def Auto.MetaState.SavedState.restore (b : SavedState) : MetaStateM Unit

Equations

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

instance Auto.MetaState.instMonadBacktrackSavedStateMetaStateM : Lean.MonadBacktrack SavedState MetaStateM

Equations

• Auto.MetaState.instMonadBacktrackSavedStateMetaStateM = { saveState := Auto.MetaState.saveState, restoreState := fun (s : Auto.MetaState.SavedState) => s.restore }

def Auto.MetaState.getToContext : MetaStateM Lean.Meta.Context

Equations

• Auto.MetaState.getToContext = do let st ← get pure st.toContext

def Auto.MetaState.setToContext (field : Lean.Meta.Context) : MetaStateM PUnit

Equations

• Auto.MetaState.setToContext field = modify fun (st : Auto.MetaState.State) => { toState := st.toState, toContext := field }

def Auto.MetaState.setToState (field : Lean.Meta.State) : MetaStateM PUnit

Equations

• Auto.MetaState.setToState field = modify fun (st : Auto.MetaState.State) => { toState := field, toContext := st.toContext }

def Auto.MetaState.getToState : MetaStateM Lean.Meta.State

Equations

• Auto.MetaState.getToState = do let st ← get pure st.toState

def Auto.MetaState.runMetaM {α : Type} (n : Lean.MetaM α) : MetaStateM α

Equations

• Auto.MetaState.runMetaM n = do let s ← get let __discr ← liftM (n.run s.toContext s.toState) match __discr with | (ret, s') => do Auto.MetaState.setToState s' pure ret

def Auto.MetaState.runAtMetaM {α : Type} (n : MetaStateM α) : Lean.MetaM (α × Lean.Meta.Context)

Equations

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

def Auto.MetaState.runAtMetaM' {α : Type} (n : MetaStateM α) : Lean.MetaM α

Run n, set State and discard context

Equations

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

def Auto.MetaState.runWithIntroducedFVars {n : Type → Type u_1} {α β : Type} [MonadControlT Lean.MetaM n] [Monad n] (m : MetaStateM (Array Lean.FVarId × α)) (k : α → n β) : n β

Equations

• Auto.MetaState.runWithIntroducedFVars m k = Lean.Meta.map1MetaM (fun {α_1 : Type} (k : α → Lean.MetaM α_1) => Auto.MetaState.runWithIntroducedFVarsImp✝ m k) k

def Auto.MetaState.inferType (e : Lean.Expr) : MetaStateM Lean.Expr

Equations

• Auto.MetaState.inferType e = Auto.MetaState.runMetaM (Lean.Meta.inferType e)

def Auto.MetaState.isDefEq (t s : Lean.Expr) : MetaStateM Bool

Equations

• Auto.MetaState.isDefEq t s = Auto.MetaState.runMetaM (Lean.Meta.isDefEq t s)

def Auto.MetaState.isDefEqRigid (t s : Lean.Expr) : MetaStateM Bool

Equations

• Auto.MetaState.isDefEqRigid t s = Auto.MetaState.runMetaM (Lean.Meta.withNewMCtxDepth (Lean.Meta.isDefEq s t))

def Auto.MetaState.isDefEqRigidWith (t s : Lean.Expr) (mode : Lean.Meta.TransparencyMode) : MetaStateM Bool

Equations

• Auto.MetaState.isDefEqRigidWith t s mode = Auto.MetaState.runMetaM (Lean.Meta.withTransparency mode (Lean.Meta.withNewMCtxDepth (Lean.Meta.isDefEq s t)))

def Auto.MetaState.isLevelDefEq (u v : Lean.Level) : MetaStateM Bool

Equations

• Auto.MetaState.isLevelDefEq u v = Auto.MetaState.runMetaM (Lean.Meta.isLevelDefEq u v)

def Auto.MetaState.isLevelDefEqRigid (u v : Lean.Level) : MetaStateM Bool

Equations

• Auto.MetaState.isLevelDefEqRigid u v = Auto.MetaState.runMetaM (Lean.Meta.withNewMCtxDepth (Lean.Meta.isLevelDefEq u v))

def Auto.MetaState.mkLocalDecl (fvarId : Lean.FVarId) (userName : Lean.Name) (type : Lean.Expr) (bi : Lean.BinderInfo := Lean.BinderInfo.default) (kind : Lean.LocalDeclKind := Lean.LocalDeclKind.default) : MetaStateM Unit

Equations

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

def Auto.MetaState.mkLetDecl (fvarId : Lean.FVarId) (userName : Lean.Name) (type value : Lean.Expr) (nonDep : Bool := false) (kind : Lean.LocalDeclKind := default) : MetaStateM Unit

Equations

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

def Auto.MetaState.withLocalDecl (n : Lean.Name) (bi : Lean.BinderInfo) (type : Lean.Expr) (kind : Lean.LocalDeclKind) : MetaStateM Lean.FVarId

Equations

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

def Auto.MetaState.withLetDecl (n : Lean.Name) (type val : Lean.Expr) (kind : Lean.LocalDeclKind) : MetaStateM Lean.FVarId

Equations

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

def Auto.MetaState.withTemporaryLCtx {n : Type → Type u_1} {α : Type} [MonadLiftT MetaStateM n] [Monad n] (lctx : Lean.LocalContext) (localInsts : Lean.LocalInstances) (k : n α) : n α

Equations

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