@[reducible, inline]

abbrev ProofWidgets.LazyEncodable (α : Type) : Type

See RpcEncodable.

Equations

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

structure ProofWidgets.ExprWithCtx : Type

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

@[instance_reducible]

instance ProofWidgets.instTypeNameExprWithCtx : TypeName ExprWithCtx

Equations

• ProofWidgets.instTypeNameExprWithCtx = ProofWidgets.inst✝

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

Equations

• e.runMetaM x = e.ci.runMetaM { } (Lean.Meta.withLCtx e.lctx e.linsts (x e.expr))

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

Equations

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