| name | hm-test |
| description | Run the HashMath test suite. Use when the user wants to run tests, check if examples pass, or verify the type checker. |
Run HashMath Tests
Run the HashMath type-checker test suite.
Instructions
-
If the argument includes "build", first rebuild the hm binary:
cd /Users/samuelschlesinger/projects/formalization/HashMath/lean && lake build hm
-
Run the test suite:
cd /Users/samuelschlesinger/projects/formalization/HashMath/lean && bash test.sh
-
Report results:
- How many examples/ files passed (should all pass)
- How many wrong/ files were correctly rejected (should all be rejected)
- Any unexpected failures or passes
Argument: $ARGUMENTS