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

structure Lean.Widget.InteractiveHypothesisBundle : Type

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.

• names : Array String

  The user-friendly name for each hypothesis. Note that these are not Names: they are pretty-printed and do not remember the macro scopes.

• 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.

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

Equations

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

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

structure Lean.Widget.InteractiveGoalCore : Type

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

• 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.

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

An interactive tactic-mode goal.

• 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.

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

Equations

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

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

An interactive term-mode goal.

• 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.

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

Equations

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

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

Equations

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

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

Equations

• Lean.Widget.InteractiveGoalCore.pretty.addLine fmt = if fmt.isNil = true then fmt else fmt ++ Lean.Format.line

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.instRpcEncodableInteractiveGoals : Lean.Server.RpcEncodable Lean.Widget.InteractiveGoals

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

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

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 (String × Lean.FVarId)) (type : Lean.Expr) (value? : 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 α

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.