# Documentation

Lean.Widget.InteractiveGoal

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

• The user-friendly name for each hypothesis.

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

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

• The hypothesis is a typeclass instance.

isInstance? :
• The hypothesis is a type.

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

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

isRemoved? :

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.

Instances For
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.
• The target type.

• Metavariable context that the goal is well-typed in.

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

Instances For
• The name foo in case foo, if any.

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

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

mvarId : Lean.MVarId
• If true, the goal was not present on the previous tactic state.

isInserted? :
• If true, the goal will be removed on the next tactic state.

isRemoved? :

An interactive tactic-mode goal.

Instances For
• Syntactic range of the term.

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

An interactive term-mode goal.

Instances For
def Lean.Widget.InteractiveGoalCore.pretty (userName? : ) (goalPrefix : String) :
Equations
• One or more equations did not get rendered due to their size.
Equations
• = if then fmt else
Equations
Equations
• goals :
Instances For
Equations
• = { goals := l.goals ++ r.goals }
Equations
def Lean.Widget.addInteractiveHypothesisBundle (ids : ) (type : Lean.Expr) (value? : optParam () none) :

Extend an array of hypothesis bundles with another bundle.

Equations
• One or more equations did not get rendered due to their size.
def Lean.Widget.withGoalCtx {n : } [inst : ] [inst : ] [inst : ] [inst : ] [inst : ] {α : Type} (goal : Lean.MVarId) (action : ) :
n α
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.