RPC procedures for retrieving tactic and term goals with embedded CodeWithInfos.
The user-friendly name for each hypothesis. If anonymous then the name is inaccessible and hidden.
- fvarIds : Array Lean.FVarId
- type : Lean.Widget.CodeWithInfos
- val? : Option Lean.Widget.CodeWithInfos
- isInstance : Bool
- isType : Bool
Equations
- One or more equations did not get rendered due to their size.
instance
Lean.Widget.instRpcEncodingInteractiveHypothesisBundleRpcEncodingPacket:
(names : Type) →
[inst : Lean.Server.RpcEncoding (Array Lean.Name) names] →
(fvarIds : Type) →
[inst : Lean.Server.RpcEncoding (Array Lean.FVarId) fvarIds] →
(type : Type) →
[inst : Lean.Server.RpcEncoding Lean.Widget.CodeWithInfos type] →
(isInstance : Type) →
[inst : Lean.Server.RpcEncoding Bool isInstance] →
Lean.Server.RpcEncoding Lean.Widget.InteractiveHypothesisBundle
(Lean.Widget.RpcEncodingPacket✝ names fvarIds type isInstance)
Equations
- One or more equations did not get rendered due to their size.
instance
Lean.Widget.instFromJsonRpcEncodingPacket_1:
{names fvarIds type isInstance : Type} →
[inst : Lean.FromJson names] →
[inst : Lean.FromJson fvarIds] →
[inst : Lean.FromJson type] →
[inst : Lean.FromJson isInstance] → Lean.FromJson (Lean.Widget.RpcEncodingPacket✝ names fvarIds type isInstance)
Equations
- Lean.Widget.instFromJsonRpcEncodingPacket_1 = { fromJson? := [anonymous] }
instance
Lean.Widget.instToJsonRpcEncodingPacket_1:
{names fvarIds type isInstance : Type} →
[inst : Lean.ToJson names] →
[inst : Lean.ToJson fvarIds] →
[inst : Lean.ToJson type] →
[inst : Lean.ToJson isInstance] → Lean.ToJson (Lean.Widget.RpcEncodingPacket✝ names fvarIds type isInstance)
Equations
- Lean.Widget.instToJsonRpcEncodingPacket_1 = { toJson := [anonymous] }
- type : Lean.Widget.CodeWithInfos
- goalPrefix : String
Identifies the goal (ie with the unique name of the MVar that it is a goal for.) This is none when we are showing a term goal.
mvarId? : Option Lean.MVarId
Equations
- Lean.Widget.instInhabitedInteractiveGoal = { default := { hyps := default, type := default, userName? := default, goalPrefix := default, mvarId? := default } }
instance
Lean.Widget.instToJsonRpcEncodingPacket_2:
{hyps type userName? mvarId? : Type} →
[inst : Lean.ToJson hyps] →
[inst : Lean.ToJson type] →
[inst : Lean.ToJson userName?] →
[inst : Lean.ToJson mvarId?] → Lean.ToJson (Lean.Widget.RpcEncodingPacket✝ hyps type userName? mvarId?)
Equations
- Lean.Widget.instToJsonRpcEncodingPacket_2 = { toJson := [anonymous] }
instance
Lean.Widget.instRpcEncodingInteractiveGoalRpcEncodingPacket:
(hyps : Type) →
[inst : Lean.Server.RpcEncoding (Array Lean.Widget.InteractiveHypothesisBundle) hyps] →
(type : Type) →
[inst : Lean.Server.RpcEncoding Lean.Widget.CodeWithInfos type] →
(userName? : Type) →
[inst : Lean.Server.RpcEncoding String userName?] →
(mvarId? : Type) →
[inst : Lean.Server.RpcEncoding Lean.MVarId mvarId?] →
Lean.Server.RpcEncoding Lean.Widget.InteractiveGoal
(Lean.Widget.RpcEncodingPacket✝ hyps type userName? mvarId?)
Equations
- One or more equations did not get rendered due to their size.
instance
Lean.Widget.instFromJsonRpcEncodingPacket_2:
{hyps type userName? mvarId? : Type} →
[inst : Lean.FromJson hyps] →
[inst : Lean.FromJson type] →
[inst : Lean.FromJson userName?] →
[inst : Lean.FromJson mvarId?] → Lean.FromJson (Lean.Widget.RpcEncodingPacket✝ hyps type userName? mvarId?)
Equations
- Lean.Widget.instFromJsonRpcEncodingPacket_2 = { fromJson? := [anonymous] }
Equations
- One or more equations did not get rendered due to their size.
- type : Lean.Widget.CodeWithInfos
- range : Lean.Lsp.Range
Equations
- Lean.Widget.instInhabitedInteractiveTermGoal = { default := { hyps := default, type := default, range := default } }
instance
Lean.Widget.instToJsonRpcEncodingPacket_3:
{hyps type range : Type} →
[inst : Lean.ToJson hyps] →
[inst : Lean.ToJson type] →
[inst : Lean.ToJson range] → Lean.ToJson (Lean.Widget.RpcEncodingPacket✝ hyps type range)
Equations
- Lean.Widget.instToJsonRpcEncodingPacket_3 = { toJson := [anonymous] }
instance
Lean.Widget.instFromJsonRpcEncodingPacket_3:
{hyps type range : Type} →
[inst : Lean.FromJson hyps] →
[inst : Lean.FromJson type] →
[inst : Lean.FromJson range] → Lean.FromJson (Lean.Widget.RpcEncodingPacket✝ hyps type range)
Equations
- Lean.Widget.instFromJsonRpcEncodingPacket_3 = { fromJson? := [anonymous] }
instance
Lean.Widget.instRpcEncodingInteractiveTermGoalRpcEncodingPacket:
(hyps : Type) →
[inst : Lean.Server.RpcEncoding (Array Lean.Widget.InteractiveHypothesisBundle) hyps] →
(type : Type) →
[inst : Lean.Server.RpcEncoding Lean.Widget.CodeWithInfos type] →
(range : Type) →
[inst : Lean.Server.RpcEncoding Lean.Lsp.Range range] →
Lean.Server.RpcEncoding Lean.Widget.InteractiveTermGoal (Lean.Widget.RpcEncodingPacket✝ hyps type range)
Equations
- One or more equations did not get rendered due to their size.
Equations
- Lean.Widget.InteractiveTermGoal.toInteractiveGoal g = { hyps := g.hyps, type := g.type, userName? := none, goalPrefix := "⊢ ", mvarId? := none }
instance
Lean.Widget.instRpcEncodingInteractiveGoalsRpcEncodingPacket:
(goals : Type) →
[inst : Lean.Server.RpcEncoding (Array Lean.Widget.InteractiveGoal) goals] →
Lean.Server.RpcEncoding Lean.Widget.InteractiveGoals (Lean.Widget.RpcEncodingPacket✝ goals)
Equations
- One or more equations did not get rendered due to their size.
instance
Lean.Widget.instFromJsonRpcEncodingPacket_4:
{goals : Type} → [inst : Lean.FromJson goals] → Lean.FromJson (Lean.Widget.RpcEncodingPacket✝ goals)
Equations
- Lean.Widget.instFromJsonRpcEncodingPacket_4 = { fromJson? := [anonymous] }
instance
Lean.Widget.instToJsonRpcEncodingPacket_4:
{goals : Type} → [inst : Lean.ToJson goals] → Lean.ToJson (Lean.Widget.RpcEncodingPacket✝ goals)
Equations
- Lean.Widget.instToJsonRpcEncodingPacket_4 = { toJson := [anonymous] }
def
Lean.Widget.addInteractiveHypothesisBundle
(hyps : Array Lean.Widget.InteractiveHypothesisBundle)
(ids : Array (Lean.Name × Lean.FVarId))
(type : Lean.Expr)
(value? : optParam (Option Lean.Expr) none)
:
Equations
- One or more equations did not get rendered due to their size.
A variant of Meta.ppGoal which preserves subexpression information for interactivity.
Equations
- One or more equations did not get rendered due to their size.