Search for declarations in the HashMath environment by name pattern. Use when the user wants to find available definitions, theorems, or types.
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.hmUnit.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