paperproof icon indicating copy to clipboard operation
paperproof copied to clipboard

Syntax assigned to tactic is incorrect

Open antonkov opened this issue 2 years ago • 0 comments

Screenshot 2024-01-04 at 01 42 01 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]. Screenshot 2024-01-04 at 01 42 47 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

antonkov avatar Jan 04 '24 01:01 antonkov