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 HashMath Declarations

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.

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.

hm-search