git.iko.soy/Idris-dev
on master help sign in
Fix definition of Field
bf4e535BlackBrane
libs/contrib/Classes/Verified.idr+2−2
compare with master
unifiedsplit
@@ -81,8 +81,8 @@ class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
81 total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
81 total ringWithUnityIsUnityR : (r : a) -> unity <.> r = r
82
82
83class (VerifiedRing a, Field a) => VerifiedField a where
83class (VerifiedRing a, Field a) => VerifiedField a where
84− total fieldInverseIsInverseL : (l : a) -> l <.> inverseM l = unity
84+ total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = unity
85− total fieldInverseIsInverseR : (r : a) -> inverseM r <.> r = unity
85+ total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = unity
86
86
87
87
88class JoinSemilattice a => VerifiedJoinSemilattice a where
88class JoinSemilattice a => VerifiedJoinSemilattice a where
libs/contrib/Control/Algebra.idr+8−8
@@ -87,10 +87,10 @@ class AbelianGroup a => Ring a where
87class Ring a => RingWithUnity a where
87class Ring a => RingWithUnity a where
88 unity : a
88 unity : a
89
89
90−||| Sets equipped with two binary operations, both associative and commutative
90+||| Sets equipped with two binary operations – both associative, commutative and
91−||| supplied with a neutral element, with
92−||| distributivity laws relating the two operations. Must satisfy the following
91+||| possessing a neutral element – and distributivity laws relating the two
93−||| laws:
92+||| operations. All elements except the additive identity must have a
93+||| multiplicative inverse. Must satisfy the following laws:
94|||
94|||
95||| + Associativity of `<+>`:
95||| + Associativity of `<+>`:
96||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
96||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c
@@ -107,14 +107,14 @@ class Ring a => RingWithUnity a where
107||| + Unity for `<.>`:
107||| + Unity for `<.>`:
108||| forall a, a <.> unity == a
108||| forall a, a <.> unity == a
109||| forall a, unity <.> a == a
109||| forall a, unity <.> a == a
110−||| + InverseM of `<.>`:
110+||| + InverseM of `<.>`, except for neutral
111−||| forall a, a <.> inverseM a == unity
111+||| forall a /= neutral, a <.> inverseM a == unity
112−||| forall a, inverseM a <.> a == unity
112+||| forall a /= neutral, inverseM a <.> a == unity
113||| + Distributivity of `<.>` and `<->`:
113||| + Distributivity of `<.>` and `<->`:
114||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
114||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)
115||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
115||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)
116class RingWithUnity a => Field a where
116class RingWithUnity a => Field a where
117− inverseM : a -> a
117+ inverseM : (x : a) -> Not (x = neutral) -> a
118
118
119
119
120-- XXX todo:
120-- XXX todo: