@[reducible, inline]

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

Instances For

• ProofWidgets.instTypeNameExprWithCtx

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

• e.runMetaM x = e.ci.runMetaM e.lctx (x e.expr)

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

Equations

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