## Stream: new members

### Topic: mathlib integer docs gcd example

#### Bryan Gin-ge Chen (Aug 09 2018 at 14:35):

The final example in this file from the mathlib docs (I guess it originally comes from this page on the xena blog) doesn't seem to typecheck for me:

import data.nat.gcd
open nat
example (m n : ℕ) : int.gcd m n = m * (gcd_a m n) + n * (gcd_b m n) := gcd_eq_gcd_ab


I get this:

type mismatch at application
m * gcd_a m n
term
gcd_a m n
has type
ℤ
but is expected to have type
ℕ


and something similar for the other summand.

#### Mario Carneiro (Aug 09 2018 at 15:01):

that should be

example (m n : ℕ) : (nat.gcd m n : ℤ) = m * (gcd_a m n) + n * (gcd_b m n) := gcd_eq_gcd_ab m n


#### Kevin Buzzard (Aug 09 2018 at 15:02):

[what Mario said]

#### Bryan Gin-ge Chen (Aug 09 2018 at 15:05):

Thanks! I was having trouble figuring out the fix by myself...

#### Patrick Massot (Aug 09 2018 at 16:05):

https://github.com/leanprover/mathlib/pull/244

#### Patrick Massot (Aug 09 2018 at 16:06):

It would be really nice to find a workflow making sure examples in the docs are correct. The manual way would be to copy them to a tests/docs/ directory, and hope things will stay synced.

#### Patrick Massot (Aug 09 2018 at 16:08):

Thanks Mario! I wonder if this is my new merge time record. I already hit some similar score a long time ago.

Last updated: May 17 2021 at 23:14 UTC