メニュー
Search for declarations in the HashMath environment by name pattern. Use when the user wants to find available definitions, theorems, or types.
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.
Run the HashMath test suite. Use when the user wants to run tests, check if examples pass, or verify the type checker.
| name | hm-search |
| description | Search for declarations in the HashMath environment by name pattern. Use when the user wants to find available definitions, theorems, or types. |
| user-invocable | true |
| allowed-tools | mcp__hm-mcp__hm_load_file, mcp__hm-mcp__hm_env, mcp__hm-mcp__hm_check, mcp__hm-mcp__hm_print, mcp__hm-mcp__hm_reset, mcp__hm-mcp__hm_read_source, Read |
| argument-hint | <search pattern> |
Search for declarations in the HashMath environment.
Call hm_reset then load the stdlib:
hm_load_file with the project's lean/stdlib/Prelude.hm
Use hm_env with the user's search pattern to find matching names.
For each interesting match, use hm_check to show its type.
If the user wants more detail about a specific declaration, use hm_print.
If they want to see the source definition, use hm_read_source on the
relevant stdlib file.
Logic.hm — True, False, And, Or, Not, Exists, IffEquality.hm — Eq, Eq.symm, Eq.trans, Eq.congr, Eq.substBool.hm — Bool, and/or/not/ite/xorUnit.hm — Unit, Empty, Empty.elimProd.hm — Prod, fst/snd/map/swapSum.hm — Sum, elim/map/swapOption.hm — Option, map/bind/getD/isSomeNat.hm — Nat, add/mul/pred, arithmetic lemmasList.hm — List, length/append/map/filter/foldr/reversePrelude.hm — imports all of the above