git.iko.soy/Idris-dev
on master help sign in
Fix definition of Field
commitbf4e5354886e224a2453759c98df6826322b1844 authorBlackBrane <cs.hbar@gmail.com> dateSat 11 Apr 2015, 18:18 (12 years ago) parent2b258db
2 files changed+10−10
compare with master
unifiedsplit
libs/contrib/Classes/Verified.idr+2−2 libs/contrib/Control/Algebra.idr+8−8
libs/contrib/Classes/Verified.idr+2−2
@@ -81,8 +81,8 @@ class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
8181 total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
8282
8383class (VerifiedRing a, Field a) => VerifiedField a where
84− total fieldInverseIsInverseL : (l : a) -> l <.> inverseM l = unity
85− total fieldInverseIsInverseR : (r : a) -> inverseM r <.> r = unity
84+ total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = unity
85+ total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = unity
8686
8787
8888class JoinSemilattice a => VerifiedJoinSemilattice a where
libs/contrib/Control/Algebra.idr+8−8
@@ -87,10 +87,10 @@ class AbelianGroup a => Ring a where
8787class Ring a => RingWithUnity a where
8888 unity : a
8989
90−||| Sets equipped with two binary operations, both associative and commutative
91−||| supplied with a neutral element, with
92−||| distributivity laws relating the two operations. Must satisfy the following
93−||| laws:
90+||| Sets equipped with two binary operations – both associative, commutative and
91+||| possessing a neutral element – and distributivity laws relating the two
92+||| operations. All elements except the additive identity must have a
93+||| multiplicative inverse. Must satisfy the following laws:
9494|||
9595||| + Associativity of `<+>`:
9696||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
@@ -107,14 +107,14 @@ class Ring a => RingWithUnity a where
107107||| + Unity for `<.>`:
108108||| forall a, a <.> unity == a
109109||| forall a, unity <.> a == a
110−||| + InverseM of `<.>`:
111−||| forall a, a <.> inverseM a == unity
112−||| forall a, inverseM a <.> a == unity
110+||| + InverseM of `<.>`, except for neutral
111+||| forall a /= neutral, a <.> inverseM a == unity
112+||| forall a /= neutral, inverseM a <.> a == unity
113113||| + Distributivity of `<.>` and `<->`:
114114||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
115115||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
116116class RingWithUnity a => Field a where
117− inverseM : a -> a
117+ inverseM : (x : a) -> Not (x = neutral) -> a
118118
119119
120120-- XXX todo: