paperproof
paperproof copied to clipboard
Syntax assigned to tactic is incorrect
For example for cases the syntax to the cases tactic is everything with all insides, but we split by
\n and therefore we display only
cases h with rw[hep].
Instead we should assign "the remaining" syntax, i.e.g only
cases h with since rw[hep] is consumed by tactic.
Or maybe it should be generated by completely different algorithm. Syntax assignment heuristic works ok-ish but definitely not always correct