mirefek

To me, it would make sense if a range could be an argument to `primes` by `primes(r::UnitRange) = primes(r.start, r.stop)` to have things such as ``` > primes(1:10) 4-element Array{Int64,1}:...

This line https://github.com/google-deepmind/alphageometry/blob/1357929e91bd327a015b26a94664035dc40b76b7/numericals.py#L705 Should not contain the parentheses, like ``` a, b, c, *ps = points ``` Otherwise, it crashes on: > TypeError: cannot unpack non-iterable Point object

Feat: Add a Html-highlighted version of #check (grayed-out implicit arguments)

3

`#checkh name` shows the signature of `name` with dimmed implicit arguments, `#checkh' name` also includes them in the String export. Zulip discussion: [#general > Dimming implicit arguments in `#check`](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Dimming.20implicit.20arguments.20in.20.60.23check.60/with/553275819)

doc: update `use` doc-string to distinguish `exists` / `use` / `use!`

3

Zulip discussion: [#general > use vs. exists @ 💬](https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/use.20vs.2E.20exists/near/562650656) --- [](https://gitpod.io/from-referrer/)