RPC procedures for retrieving tactic and term goals with embedded CodeWithInfos.

structure Lean.Widget.InteractiveHypothesisBundle : Type

• The user-friendly name for each hypothesis. If anonymous then the name is inaccessible and hidden.

  names : Array Lean.Name

• The ids for each variable. Should have the same length as names.

  fvarIds : Array Lean.FVarId
• type : Lean.Widget.CodeWithInfos

• The value, in the case the hypothesis is a let-binder.

  val? : Option Lean.Widget.CodeWithInfos

• The hypothesis is a typeclass instance.

  isInstance : Bool

• The hypothesis is a type.

  isType : Bool

• If true, the hypothesis was not present on the previous tactic state. Uses none instead of some false to save space in the json encoding.

  isInserted? : Option Bool

• If true, the hypothesis will be removed in the next tactic state. Uses none instead of some false to save space in the json encoding.

  isRemoved? : Option Bool

In the infoview, if multiple hypotheses h₁, h₂ have the same type α, they are rendered as h₁ h₂ : α. We call this a 'hypothesis bundle'.

instance Lean.Widget.instInhabitedInteractiveHypothesisBundle : Inhabited Lean.Widget.InteractiveHypothesisBundle

Equations

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

instance Lean.Widget.instToJsonRpcEncodablePacket_1 : Lean.ToJson Lean.Widget.RpcEncodablePacket✝

Equations

• Lean.Widget.instToJsonRpcEncodablePacket_1 = { toJson := Lean.Widget.toJsonRpcEncodablePacket✝ }

instance Lean.Widget.instRpcEncodableInteractiveHypothesisBundle : Lean.Server.RpcEncodable Lean.Widget.InteractiveHypothesisBundle

Equations

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

instance Lean.Widget.instFromJsonRpcEncodablePacket_1 : Lean.FromJson Lean.Widget.RpcEncodablePacket✝

Equations

• Lean.Widget.instFromJsonRpcEncodablePacket_1 = { fromJson? := Lean.Widget.fromJsonRpcEncodablePacket✝ }

structure Lean.Widget.InteractiveGoal : Type

• hyps : Array Lean.Widget.InteractiveHypothesisBundle
• type : Lean.Widget.CodeWithInfos
• userName? : Option String
• 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

• If true, the goal was not present on the previous tactic state. Uses none instead of some false to save space in the json encoding.

  isInserted? : Option Bool

• If true, the goal will be removed on the next tactic state. Uses none instead of some false to save space in the json encoding.

  isRemoved? : Option Bool

instance Lean.Widget.instInhabitedInteractiveGoal : Inhabited Lean.Widget.InteractiveGoal

Equations

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

instance Lean.Widget.instFromJsonRpcEncodablePacket_2 : Lean.FromJson Lean.Widget.RpcEncodablePacket✝

Equations

• Lean.Widget.instFromJsonRpcEncodablePacket_2 = { fromJson? := Lean.Widget.fromJsonRpcEncodablePacket✝ }

instance Lean.Widget.instToJsonRpcEncodablePacket_2 : Lean.ToJson Lean.Widget.RpcEncodablePacket✝

Equations

• Lean.Widget.instToJsonRpcEncodablePacket_2 = { toJson := Lean.Widget.toJsonRpcEncodablePacket✝ }

instance Lean.Widget.instRpcEncodableInteractiveGoal : Lean.Server.RpcEncodable Lean.Widget.InteractiveGoal

Equations

• Lean.Widget.instRpcEncodableInteractiveGoal = { rpcEncode := Lean.Widget.instRpcEncodableInteractiveGoal.enc✝, rpcDecode := Lean.Widget.instRpcEncodableInteractiveGoal.dec✝ }

def Lean.Widget.InteractiveGoal.pretty (g : Lean.Widget.InteractiveGoal) : Lean.Format

Equations

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

structure Lean.Widget.InteractiveTermGoal : Type

• hyps : Array Lean.Widget.InteractiveHypothesisBundle
• type : Lean.Widget.CodeWithInfos
• range : Lean.Lsp.Range

This is everything needed to render an interactive term goal in the infoview.

instance Lean.Widget.instInhabitedInteractiveTermGoal : Inhabited Lean.Widget.InteractiveTermGoal

Equations

• Lean.Widget.instInhabitedInteractiveTermGoal = { default := { hyps := default, type := default, range := default } }

instance Lean.Widget.instRpcEncodableInteractiveTermGoal : Lean.Server.RpcEncodable Lean.Widget.InteractiveTermGoal

Equations

• Lean.Widget.instRpcEncodableInteractiveTermGoal = { rpcEncode := Lean.Widget.instRpcEncodableInteractiveTermGoal.enc✝, rpcDecode := Lean.Widget.instRpcEncodableInteractiveTermGoal.dec✝ }

instance Lean.Widget.instToJsonRpcEncodablePacket_3 : Lean.ToJson Lean.Widget.RpcEncodablePacket✝

Equations

• Lean.Widget.instToJsonRpcEncodablePacket_3 = { toJson := Lean.Widget.toJsonRpcEncodablePacket✝ }

instance Lean.Widget.instFromJsonRpcEncodablePacket_3 : Lean.FromJson Lean.Widget.RpcEncodablePacket✝

Equations

• Lean.Widget.instFromJsonRpcEncodablePacket_3 = { fromJson? := Lean.Widget.fromJsonRpcEncodablePacket✝ }

def Lean.Widget.InteractiveTermGoal.toInteractiveGoal (g : Lean.Widget.InteractiveTermGoal) : Lean.Widget.InteractiveGoal

Equations

• Lean.Widget.InteractiveTermGoal.toInteractiveGoal g = { hyps := g.hyps, type := g.type, userName? := none, goalPrefix := "⊢ ", mvarId? := none, isInserted? := none, isRemoved? := none }

structure Lean.Widget.InteractiveGoals : Type

• goals : Array Lean.Widget.InteractiveGoal

instance Lean.Widget.instRpcEncodableInteractiveGoals : Lean.Server.RpcEncodable Lean.Widget.InteractiveGoals

Equations

• Lean.Widget.instRpcEncodableInteractiveGoals = { rpcEncode := Lean.Widget.instRpcEncodableInteractiveGoals.enc✝, rpcDecode := Lean.Widget.instRpcEncodableInteractiveGoals.dec✝ }

instance Lean.Widget.instToJsonRpcEncodablePacket_4 : Lean.ToJson Lean.Widget.RpcEncodablePacket✝

Equations

• Lean.Widget.instToJsonRpcEncodablePacket_4 = { toJson := Lean.Widget.toJsonRpcEncodablePacket✝ }

instance Lean.Widget.instFromJsonRpcEncodablePacket_4 : Lean.FromJson Lean.Widget.RpcEncodablePacket✝

Equations

• Lean.Widget.instFromJsonRpcEncodablePacket_4 = { fromJson? := Lean.Widget.fromJsonRpcEncodablePacket✝ }

def Lean.Widget.InteractiveGoals.append (l : Lean.Widget.InteractiveGoals) (r : Lean.Widget.InteractiveGoals) : Lean.Widget.InteractiveGoals

Equations

• Lean.Widget.InteractiveGoals.append l r = { goals := l.goals ++ r.goals }

instance Lean.Widget.instAppendInteractiveGoals : Append Lean.Widget.InteractiveGoals

Equations

• Lean.Widget.instAppendInteractiveGoals = { append := Lean.Widget.InteractiveGoals.append }

instance Lean.Widget.instEmptyCollectionInteractiveGoals : EmptyCollection Lean.Widget.InteractiveGoals

Equations

• Lean.Widget.instEmptyCollectionInteractiveGoals = { emptyCollection := { goals := #[] } }

def Lean.Widget.addInteractiveHypothesisBundle (hyps : Array Lean.Widget.InteractiveHypothesisBundle) (ids : Array (Lean.Name × Lean.FVarId)) (type : Lean.Expr) (value? : optParam (Option Lean.Expr) none) : Lean.MetaM (Array Lean.Widget.InteractiveHypothesisBundle)

Equations

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

def Lean.Widget.withGoalCtx {n : Type → Type} [inst : MonadControlT Lean.MetaM n] [inst : Monad n] [inst : Lean.MonadError n] [inst : Lean.MonadOptions n] [inst : Lean.MonadMCtx n] {α : Type} (goal : Lean.MVarId) (action : Lean.LocalContext → Lean.MetavarDecl → n α) : n α

Equations

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

def Lean.Widget.goalToInteractive (mvarId : Lean.MVarId) : Lean.MetaM Lean.Widget.InteractiveGoal

A variant of Meta.ppGoal which preserves subexpression information for interactivity.

Equations

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