lean4game icon indicating copy to clipboard operation
lean4game copied to clipboard
verified publisher icon leanprover-community

Increase severity of `uses 'sorry'`. Fixes #276

Open tautastic opened this issue 1 year ago • 0 comments

Increase severity of uses 'sorry'. Fixes #276. The goal will no longer be considered completed but the actual syntax error is not displayed anywhere.

tautastic avatar Feb 26 '25 18:02 tautastic