Zulip Chat Archive

Stream: new members

Topic: gcd


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Lacker (Sep 30 2020 at 18:28):

so everything under that "init" directory is automatically imported?

view this post on Zulip 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