Functionality related to tactic-mode and term-mode goals with embedded CodeWithInfos
.
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.
The user-friendly name for each hypothesis. Note that these are not
Name
s: 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. The hypothesis is a typeclass instance.
The hypothesis is a type.
If true, the hypothesis was not present on the previous tactic state. Only present in tactic-mode goals.
If true, the hypothesis will be removed in the next tactic state. Only present in tactic-mode goals.
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 shared parts of interactive term-mode and tactic-mode goals.
- type : Lean.Widget.CodeWithInfos
The target type.
Metavariable context that the goal is well-typed in.
Instances For
An interactive tactic-mode goal.
- type : Lean.Widget.CodeWithInfos
The name
foo
incase foo
, if any.- goalPrefix : String
The symbol to display before the target type. Usually
⊢
butconv
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.)
If true, the goal was not present on the previous tactic state.
If true, the goal will be removed on the next tactic state.
Instances For
Equations
- One or more equations did not get rendered due to their size.
An interactive term-mode goal.
- type : Lean.Widget.CodeWithInfos
- range : Lean.Lsp.Range
Syntactic range of the term.
Information about the term whose type is the term-mode goal.
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.
Instances For
Equations
- Lean.Widget.InteractiveGoalCore.pretty.addLine fmt = if fmt.isNil = true then fmt else fmt ++ Lean.Format.line
Instances For
Equations
- g.pretty = g.pretty g.userName? g.goalPrefix
Instances For
Equations
- g.pretty = g.pretty none "⊢ "
Instances For
- goals : Array Lean.Widget.InteractiveGoal
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lean.Widget.instEmptyCollectionInteractiveGoals = { emptyCollection := { goals := #[] } }
Extend an array of hypothesis bundles with another bundle.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
A variant of Meta.ppGoal
which preserves subexpression information for interactivity.
Equations
- One or more equations did not get rendered due to their size.