Skip to content

Commit

Permalink
cleanup during tests
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Nov 16, 2023
1 parent 13087b3 commit 6379774
Showing 1 changed file with 4 additions and 0 deletions.
4 changes: 4 additions & 0 deletions test.sh
Original file line number Diff line number Diff line change
Expand Up @@ -34,6 +34,10 @@ check_command "lake exe lean4checker Lean4Checker.Tests.AddFalseConstructor" "un

check_command "lake exe lean4checker --fresh Lean4Checker.Tests.UseFalseConstructor" "uncaught exception: (kernel) unknown constant 'False.intro'"

rm -f .lean4checker.tmp

check_command "lake exe lean4checker Lean4Checker.Tests.ReduceBool" "uncaught exception: (kernel) unknown declaration 'foo'"

rm -f .lean4checker.tmp

echo "All commands produced the expected errors."

0 comments on commit 6379774

Please sign in to comment.