Stream: new members
Bryan Gin-ge Chen (Aug 09 2018 at 14:35):
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):
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