Stream: new members

Topic: gcd

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