@[inline, reducible]

abbrev ProofWidgets.LazyEncodable (α : Type) : Type

Equations

• ProofWidgets.LazyEncodable α = StateM Lean.Server.RpcObjectStore α

structure ProofWidgets.ExprWithCtx : Type

• ci : Lean.Elab.ContextInfo
• lctx : Lean.LocalContext
• expr : Lean.Expr

instance ProofWidgets.instTypeNameExprWithCtx : TypeName ProofWidgets.ExprWithCtx

Equations

• ProofWidgets.instTypeNameExprWithCtx = ProofWidgets.inst✝

def ProofWidgets.ExprWithCtx.runMetaM {α : Type} (e : ProofWidgets.ExprWithCtx) (x : Lean.Expr → Lean.MetaM α) : IO α

Equations

• ProofWidgets.ExprWithCtx.runMetaM e x = Lean.Elab.ContextInfo.runMetaM e.ci e.lctx (x e.expr)

def ProofWidgets.ExprWithCtx.save (e : Lean.Expr) : Lean.MetaM ProofWidgets.ExprWithCtx

Equations

• ProofWidgets.ExprWithCtx.save e = do let __do_lift ← Lean.Elab.ContextInfo.save let __do_lift_1 ← Lean.getLCtx pure { ci := __do_lift, lctx := __do_lift_1, expr := e }