These are chat archives for non/algebra

20th
Sep 2016
Denis Rosset
@denisrosset
Sep 20 2016 06:03
I had a look at the EuclideanRing typeclass, instances and laws. The typeclass and the expressed laws are correct. However, we don't have any tests for the Euclidean function property, I am going to fill the gap.
My suspicion is that the Rational/Float/Double instances will be not lawful.
Will submit a PR later today.
Tom Switzer
@tixxit
Sep 20 2016 17:45
Interesting - fwiw, I was mostly trying to match other tool's behaviour
Lars Hupel
@larsrh
Sep 20 2016 18:03
@tixxit Not everyone agrees on that result, though
In Isabelle gcd(1/2, 1/3) is 1
But gcd is gone now from algebra, right?
Tom Switzer
@tixxit
Sep 20 2016 18:37
@larsrh yeah - this is really about Spire, just the wrong channel