In incomplete match statements and in incomplete terms in apply, the elaborator often does not produce InfoTrees.
Context
This issue is derived from #5172. #5299 resolves the fact that completion doesn't trigger in these contexts, but it doesn't resolve the underlying problem that the elaborator does not produce InfoTrees in this example, which are also needed for all kinds of other language server features.
Steps to Reproduce
Consider the following example from #5172:
set_option trace.Elab.info true
inductive Direction where
| up
| right
| down
| left
deriving Repr
def angle (d: Direction) :=
match d with
| Direction. => 90
| Direction.right => 0
| Direction.down => 270
| Direction.left => 180
example : p ∨ (q ∧ r) → (p ∨ q) ∧ (p ∨ r) := by
intro h
cases h with
| inl hp => apply And. (Or.intro_left q hp) (Or.intro_left r hp)
| inr hqr => apply And.intro (Or.intro_right p hqr.left) (Or.intro_right p hqr.right)
In angle, all InfoTree information for the incomplete match statement is missing. In the example, all InfoTree information for the incomplete term in the first apply is missing.
Description
In incomplete
match
statements and in incomplete terms inapply
, the elaborator often does not produceInfoTree
s.Context
This issue is derived from #5172. #5299 resolves the fact that completion doesn't trigger in these contexts, but it doesn't resolve the underlying problem that the elaborator does not produce InfoTrees in this example, which are also needed for all kinds of other language server features.
Steps to Reproduce
Consider the following example from #5172:
In
angle
, allInfoTree
information for the incompletematch
statement is missing. In theexample
, allInfoTree
information for the incomplete term in the firstapply
is missing.Versions
Current master (ec98c92).
Impact
Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.