source
@[reducible, inline]
abbrev ProofWidgets.LazyEncodable (α : Type) :
Type
Equations

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

Instances For

source
structure ProofWidgets.ExprWithCtx :
Type

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

Instances For

source
instance ProofWidgets.instTypeNameExprWithCtx :
TypeName ExprWithCtx
Equations

- ProofWidgets.instTypeNameExprWithCtx = ProofWidgets.inst✝

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

Instances For

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

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

Instances For