菜单
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