Functionality related to tactic-mode and term-mode goals with embedded
The user-friendly name for each hypothesis.
The ids for each variable. Should have the same length as
The value, in the case the hypothesis is a
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.
In the infoview, if multiple hypotheses
h₂ have the same type
α, they are rendered
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 target type.
Metavariable context that the goal is well-typed in.
The shared parts of interactive term-mode and tactic-mode goals.
case foo, if any.
- goalPrefix : String
The symbol to display before the target type. Usually
∣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.
An interactive tactic-mode goal.
- range : Lean.Lsp.Range
Syntactic range of the term.
Information about the term whose type is the term-mode goal.
An interactive term-mode goal.
Extend an array of hypothesis bundles with another bundle.