mathlib integer docs gcd example

Stream: new members

[Bryan Gin-ge Chen]

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]

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]

[what Mario said]

[Bryan Gin-ge Chen]

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

[Patrick Massot]

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

[Patrick Massot]

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]

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