structure Lean.Widget.InfoWithCtx : Type

• ctx : Lean.Elab.ContextInfo
• info : Lean.Elab.Info

Elaborator information with elaborator context.

This is used to tag different parts of expressions in ppExprTagged. This is the input to the RPC call Lean.Widget.InteractiveDiagnostics.infoToInteractive.

The purpose of InfoWithCtx is to carry over information about delaborated Info nodes in a CodeWithInfos, and the associated pretty-printing functionality is purpose-specific to showing the contents of infoview popups.

instance Lean.Widget.instTypeNameInfoWithCtx : TypeName Lean.Widget.InfoWithCtx

Equations

• Lean.Widget.instTypeNameInfoWithCtx = Lean.Widget.inst✝

instance Lean.Widget.instTypeNameMessageData : TypeName Lean.MessageData

Equations

• Lean.Widget.instTypeNameMessageData = Lean.Widget.inst✝

instance Lean.Widget.instToJsonFVarId : Lean.ToJson Lean.FVarId

Equations

• Lean.Widget.instToJsonFVarId = { toJson := fun f => Lean.toJson f.name }

instance Lean.Widget.instToJsonMVarId : Lean.ToJson Lean.MVarId

Equations

• Lean.Widget.instToJsonMVarId = { toJson := fun f => Lean.toJson f.name }

instance Lean.Widget.instFromJsonFVarId : Lean.FromJson Lean.FVarId

Equations

• Lean.Widget.instFromJsonFVarId = { fromJson? := fun j => Lean.FVarId.mk <$> Lean.fromJson? j }

instance Lean.Widget.instFromJsonMVarId : Lean.FromJson Lean.MVarId

Equations

• Lean.Widget.instFromJsonMVarId = { fromJson? := fun j => Lean.MVarId.mk <$> Lean.fromJson? j }