search

ekmett / algebra

constructive abstract algebra
http://hackage.haskell.org/package/algebra
Other
101 stars 14 forks source link

The documented contract for splitUnit is too weak #9

Closed dfoxfranke closed 8 years ago

dfoxfranke commented 9 years ago

splitUnit is currently specified as follows:

let (u, n) = splitUnit r in r == u * n && fst (splitUnit n) == one && isUnit u

This condition is too weak and can be always be satsified by splitUnit r = (one,r). EuclideanDomain should inherit from DecidableAssociates and, letting (u',n') = splitUnit r', the specification should require that n == n' <-> isAssociate r r'.