Syntax assigned to tactic is incorrect
antonkov opened this issue · 0 comments
antonkov commented
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