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 FVarId

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

• type : CodeWithInfos
• val? : Option 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.

def Lean.Widget.instInhabitedInteractiveHypothesisBundle.default : InteractiveHypothesisBundle

Equations

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

instance Lean.Widget.instInhabitedInteractiveHypothesisBundle : Inhabited InteractiveHypothesisBundle

Equations

• Lean.Widget.instInhabitedInteractiveHypothesisBundle = { default := Lean.Widget.instInhabitedInteractiveHypothesisBundle.default }

instance Lean.Widget.instRpcEncodableInteractiveHypothesisBundle : Server.RpcEncodable InteractiveHypothesisBundle

Equations

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

structure Lean.Widget.InteractiveGoalCore : Type

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

• hyps : Array InteractiveHypothesisBundle
• type : CodeWithInfos

  The target type.

• ctx : Server.WithRpcRef 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 InteractiveHypothesisBundle
• type : CodeWithInfos
• ctx : Server.WithRpcRef 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 : 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 : Server.RpcEncodable 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 InteractiveHypothesisBundle
• type : CodeWithInfos
• ctx : Server.WithRpcRef Elab.ContextInfo
• range : Lsp.Range

  Syntactic range of the term.

• term : Server.WithRpcRef Elab.TermInfo

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

instance Lean.Widget.instRpcEncodableInteractiveTermGoal : Server.RpcEncodable InteractiveTermGoal

Equations

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

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

Equations

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

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

Equations

• g.pretty = g.pretty g.userName? g.goalPrefix

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

Equations

• g.pretty = g.pretty none "⊢ "

structure Lean.Widget.InteractiveGoals : Type

• goals : Array InteractiveGoal

instance Lean.Widget.instRpcEncodableInteractiveGoals : Server.RpcEncodable InteractiveGoals

Equations

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

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

Equations

• l.append r = { goals := l.goals ++ r.goals }

instance Lean.Widget.instAppendInteractiveGoals : Append InteractiveGoals

Equations

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

instance Lean.Widget.instEmptyCollectionInteractiveGoals : EmptyCollection InteractiveGoals

Equations

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

def Lean.Widget.addInteractiveHypothesisBundle (hyps : Array InteractiveHypothesisBundle) (ids : Array (String × FVarId)) (type : Expr) (value? : Option Expr := none) (tactic : Bool := false) : MetaM (Array InteractiveHypothesisBundle)

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 : Type → Type} [MonadControlT MetaM n] [Monad n] [MonadError n] [MonadOptions n] [MonadMCtx n] {α : Type} (goal : MVarId) (action : LocalContext → MetavarDecl → n α) : n α

Equations

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

def Lean.Widget.goalToInteractive (mvarId : MVarId) : MetaM 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.