Zulip Chat Archive

Stream: new members

Topic: mathlib integer docs gcd example


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

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

view this post on Zulip Kevin Buzzard (Aug 09 2018 at 15:02):

[what Mario said]

view this post on Zulip Bryan Gin-ge Chen (Aug 09 2018 at 15:05):

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

view this post on Zulip Patrick Massot (Aug 09 2018 at 16:05):

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

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

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