arend-lib icon indicating copy to clipboard operation
arend-lib copied to clipboard

Not intuitive error message of mcases tactic.

Open sxhya opened this issue 6 months ago • 0 comments

If the user forgets to surround mcases tactic with parentheses he won't get an error message. Instead he will get "missing clauses" message (despite the fact that clauses are present and no syntactic error is reported!)

image

sxhya avatar Sep 03 '24 09:09 sxhya