Zulip Chat Archive

Hi! Is there a search engine (web or cli based) for symbols and types, such as hoogle for haskell? I find it hard and time consuming searching in the API by hand, especially if you are new to lean. For example, searching for "\N -> \Z" should find "neg_of_nat", and searching "neg" should also find "neg_of_nat".

Eric Wieser (Oct 22 2021 at 20:01):

There's #find which should work for that first case

Eric Wieser (Oct 22 2021 at 20:02):

And the online docs have a search bar, it takes a little while to start autosuggesting.

Kyle Miller (Oct 22 2021 at 20:03):

From within a random file I had open:

#find ℕ → ℤ
/- gives:
linarith.linexp.zfind: ℕ → linarith.linexp → ℤ
nat.gcd_b: ℕ → ℕ → ℤ
nat.gcd_a: ℕ → ℕ → ℤ
linarith.comp.coeff_of: linarith.comp → ℕ → ℤ
int.sub_nat_nat: ℕ → ℕ → ℤ
zmod.val_min_abs: Π {n : ℕ}, zmod n → ℤ
int.nat_bitwise: (bool → bool → bool) → ℕ → ℕ → ℤ
int.neg_of_nat: ℕ → ℤ
-/

Kyle Miller (Oct 22 2021 at 20:04):

example : ℕ → ℤ := by suggest
/- gives:
Try this: exact int.of_nat
Try this: exact int.neg_of_nat
Try this: exact int.neg_succ_of_nat
Try this: refine nat.gcd_a _
Try this: refine nat.gcd_b _
Try this: refine int.sub_nat_nat _
Try this: refine linarith.comp.coeff_of _
Try this: refine int.nat_bitwise _ _
-/