- 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.
Equations
- Lean.Widget.instInhabitedInfoWithCtx = { default := { ctx := default, info := default } }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Widget.instToJsonFVarId = { toJson := fun f => Lean.toJson f.name }
Equations
- Lean.Widget.instToJsonMVarId = { toJson := fun f => Lean.toJson f.name }
Equations
- Lean.Widget.instFromJsonFVarId = { fromJson? := fun j => Lean.FVarId.mk <$> Lean.fromJson? j }
Equations
- Lean.Widget.instFromJsonMVarId = { fromJson? := fun j => Lean.MVarId.mk <$> Lean.fromJson? j }