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

structure Lean.Widget.InteractiveHypothesisBundle : Type

• The user-friendly name for each hypothesis.

  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? : Option Bool

• The hypothesis is a type.

  isType? : Option Bool

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

  isInserted? : Option Bool

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

  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'. We use none instead of some false for booleans to save space in the json encoding.

instance Lean.Widget.instInhabitedInteractiveHypothesisBundle : Inhabited 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✝ }

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.instToJsonRpcEncodablePacket_1 : Lean.ToJson Lean.Widget.RpcEncodablePacket✝

Equations

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

structure Lean.Widget.InteractiveGoalCore : Type

• hyps : Array Lean.Widget.InteractiveHypothesisBundle

• The target type.

  type : Lean.Widget.CodeWithInfos

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

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

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

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

• The name foo in case foo, if any.

  userName? : Option String

• 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? : Option Bool

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

  isRemoved? : Option Bool

An interactive tactic-mode goal.

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

Equations

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

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

Equations

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

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

• Syntactic range of the term.

  range : Lean.Lsp.Range

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

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

An interactive term-mode goal.

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

Equations

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

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✝ }

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 Std.Format.isNil fmt = true then fmt else fmt ++ Lean.Format.line

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

Equations

• Lean.Widget.InteractiveGoal.pretty g = Lean.Widget.InteractiveGoalCore.pretty g.toInteractiveGoalCore g.userName? g.goalPrefix

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

Equations

• Lean.Widget.InteractiveTermGoal.pretty g = Lean.Widget.InteractiveGoalCore.pretty g.toInteractiveGoalCore none "⊢ "

structure Lean.Widget.InteractiveGoals : Type

• goals : Array Lean.Widget.InteractiveGoal

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

Equations

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

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

Equations

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

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

Equations

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

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)

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} [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.