Stream: new members
Kevin Lacker (Sep 30 2020 at 18:25):
new navigating-the-docs question. I'm looking for where
gcd is defined. search leads me to https://github.com/leanprover-community/mathlib/blob/5fd2037/src/data/nat/gcd.lean#L162 which has a comment saying, here is where gcd is defined. however, there doesn't actually seem to be a definition here? it only imports one file, https://github.com/leanprover-community/mathlib/blob/5fd2037/src/data/nat/basic.lean , but that file doesn't mention "gcd" at all. 1/ where is gcd defined, and 2/ what is the right way for me to discover this for myself
Bryan Gin-ge Chen (Sep 30 2020 at 18:26):
It's defined in core: docs#nat.gcd
If you type
nat.gcd into the search window and wait (don't hit "search"!) then choose the first option, it should take you to this declaration.
Bryan Gin-ge Chen (Sep 30 2020 at 18:27):
In emacs it should be possible to peek / navigate to the definition of
nat.gcd, which is another way of finding out where any given definition is.
Kevin Lacker (Sep 30 2020 at 18:28):
so everything under that "init" directory is automatically imported?
Bryan Gin-ge Chen (Sep 30 2020 at 18:29):
Yep, unless you put
prelude at the top of your file.
Last updated: May 11 2021 at 22:14 UTC