메뉴
Run the HashMath test suite. Use when the user wants to run tests, check if examples pass, or verify the type checker.
Codex 또는 Claude로 설치 이 Prompt를 복사해 Codex, Claude 또는 다른 어시스턴트에 붙여 넣으면 Skill 페이지를 검토하고 설치를 진행할 수 있습니다.
SOC 직업 분류 기준
Type-check HashMath (.hm) source code or files. Use when the user wants to verify that .hm code type-checks correctly.
Help prove a theorem in HashMath. Use when the user wants to construct a proof term, define a theorem, or needs help writing .hm proof code.
Search for declarations in the HashMath environment by name pattern. Use when the user wants to find available definitions, theorems, or types.
| 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 the HashMath type-checker test suite.
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: