Functionality related to tactic-mode and term-mode goals with embedded CodeWithInfos.

structure Lean.Widget.InteractiveHypothesisBundle : Type

• names : Array Lake.Name

  The user-friendly name for each hypothesis.

• fvarIds : Array Lean.FVarId

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

• type : Lean.Widget.CodeWithInfos
• val? : Option Lean.Widget.CodeWithInfos

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

• isInstance? : Option Bool

  The hypothesis is a typeclass instance.

• isType? : Option Bool

  The hypothesis is a type.

• isInserted? : Option Bool

  If true, the hypothesis was not present on the previous tactic state. Only present in tactic-mode goals.

• isRemoved? : Option Bool

  If true, the hypothesis will be removed in the next tactic state. Only present in tactic-mode goals.

In the infoview, if multiple hypotheses h₁, h₂ have the same type α, they are rendered as h₁ h₂ : α. We call this a 'hypothesis bundle'. We use none instead of some false for booleans to save space in the json encoding.

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

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

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

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

structure Lean.Widget.InteractiveGoalCore : Type

• hyps : Array Lean.Widget.InteractiveHypothesisBundle
• type : Lean.Widget.CodeWithInfos

  The target type.

• ctx : Lean.Server.WithRpcRef Lean.Elab.ContextInfo

  Metavariable context that the goal is well-typed in.

The shared parts of interactive term-mode and tactic-mode goals.

structure Lean.Widget.InteractiveGoalextends Lean.Widget.InteractiveGoalCore : Type

• hyps : Array Lean.Widget.InteractiveHypothesisBundle
• type : Lean.Widget.CodeWithInfos
• ctx : Lean.Server.WithRpcRef Lean.Elab.ContextInfo
• userName? : Option String

  The name foo in case foo, if any.

• goalPrefix : String

  The symbol to display before the target type. Usually ⊢ but conv goals use ∣ and it could be extended.

• mvarId : Lean.MVarId

  Identifies the goal (ie with the unique name of the MVar that it is a goal for.)

• isInserted? : Option Bool

  If true, the goal was not present on the previous tactic state.

• isRemoved? : Option Bool

  If true, the goal will be removed on the next tactic state.

An interactive tactic-mode goal.

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

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

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

structure Lean.Widget.InteractiveTermGoalextends Lean.Widget.InteractiveGoalCore : Type

• hyps : Array Lean.Widget.InteractiveHypothesisBundle
• type : Lean.Widget.CodeWithInfos
• ctx : Lean.Server.WithRpcRef Lean.Elab.ContextInfo
• range : Lean.Lsp.Range

  Syntactic range of the term.

• term : Lean.Server.WithRpcRef Lean.Elab.TermInfo

  Information about the term whose type is the term-mode goal.

An interactive term-mode goal.

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

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

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

def Lean.Widget.InteractiveGoalCore.pretty (g : Lean.Widget.InteractiveGoalCore) (userName? : Option String) (goalPrefix : String) : Lean.Format

def Lean.Widget.InteractiveGoalCore.pretty.addLine (fmt : Lean.Format) : Lean.Format

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

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

structure Lean.Widget.InteractiveGoals : Type

• goals : Array Lean.Widget.InteractiveGoal

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

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

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

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

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

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

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

Extend an array of hypothesis bundles with another bundle.

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

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

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