Documentation

Lean.Widget.InteractiveCode

RPC infrastructure for storing and formatting code fragments, in particular Exprs, with environment and subexpression information.

source
structure Lean.Widget.SubexprInfo:
Type

Information about a subexpression within delaborated code.

source
instance Lean.Widget.instInhabitedSubexprInfo:
Inhabited Lean.Widget.SubexprInfo
Equations
source
instance Lean.Widget.instToJsonRpcEncodingPacket:
{info subexprPos : Type} → [inst : Lean.ToJson info] → [inst : Lean.ToJson subexprPos] → Lean.ToJson (Lean.Widget.RpcEncodingPacket✝ info subexprPos)
Equations
  • Lean.Widget.instToJsonRpcEncodingPacket = { toJson := [anonymous] }
source
instance Lean.Widget.instFromJsonRpcEncodingPacket:
{info subexprPos : Type} → [inst : Lean.FromJson info] → [inst : Lean.FromJson subexprPos] → Lean.FromJson (Lean.Widget.RpcEncodingPacket✝ info subexprPos)
Equations
  • Lean.Widget.instFromJsonRpcEncodingPacket = { fromJson? := [anonymous] }
source
instance Lean.Widget.instRpcEncodingSubexprInfoRpcEncodingPacket:
(info : Type) → [inst : Lean.Server.RpcEncoding (Lean.Server.WithRpcRef Lean.Widget.InfoWithCtx) info] → (subexprPos : Type) → [inst : Lean.Server.RpcEncoding Lean.SubExpr.Pos subexprPos] → Lean.Server.RpcEncoding Lean.Widget.SubexprInfo (Lean.Widget.RpcEncodingPacket✝ info subexprPos)
Equations
  • One or more equations did not get rendered due to their size.
source
@[inline]
abbrev Lean.Widget.CodeWithInfos:
Type

Pretty-printed syntax (usually but not necessarily an Expr) with embedded Infos.

Equations
source
def Lean.Widget.CodeWithInfos.pretty (tt : Lean.Widget.CodeWithInfos) :
String
Equations
source
def Lean.Widget.tagExprInfos (ctx : Lean.Elab.ContextInfo) (infos : Std.RBMap Nat Lean.Elab.Info compare) (tt : Lean.Widget.TaggedText (Nat × Nat)) :
Lean.Widget.CodeWithInfos

Tags a pretty-printed Expr with infos from the delaborator.

Equations
source
partial def Lean.Widget.tagExprInfos.go (ctx : Lean.Elab.ContextInfo) (infos : Std.RBMap Nat Lean.Elab.Info compare) (tt : Lean.Widget.TaggedText (Nat × Nat)) :
Lean.Widget.TaggedText Lean.Widget.SubexprInfo
source
def Lean.Widget.ppExprTagged (e : Lean.Expr) (explicit : optParam Bool false) :
Lean.MetaM Lean.Widget.CodeWithInfos
Equations
  • One or more equations did not get rendered due to their size.