@@ -35,8 +35,8 @@ class Semigroup a => Monoid a where
35 neutral : a
35 neutral : a
37class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
37class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
38− monoidIsNeutralL : (l : a) -> l <+> neutral = l
38+ monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l
39− monoidIsNeutralR : (r : a) -> neutral <+> r = r
39+ monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r
41-- Sets equipped with a single binary operation that is associative, along with
41-- Sets equipped with a single binary operation that is associative, along with
42-- a neutral element for that binary operation and inverses for all elements.
42-- a neutral element for that binary operation and inverses for all elements.
@@ -100,9 +100,9 @@ class AbelianGroup a => Ring a where
100 (<*>) : a -> a -> a
100 (<*>) : a -> a -> a
102class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
102class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
103− ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
103+ ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
104− ringOpsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)
104+ ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)
105− ringOpsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)
105+ ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)
107-- Sets equipped with two binary operations, one associative and commutative
107-- Sets equipped with two binary operations, one associative and commutative
108-- supplied with a neutral element, and the other associative supplied with a
108-- supplied with a neutral element, and the other associative supplied with a
@@ -163,9 +163,9 @@ class MeetSemilattice a where
163 meet : a -> a -> a
163 meet : a -> a -> a
165class MeetSemilattice a => VerifiedMeetSemilattice a where
165class MeetSemilattice a => VerifiedMeetSemilattice a where
166− meetSemilatticeJoinIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
166+ meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
167− meetSemilatticeJoinIsCommutative : (l, r : a) -> meet l r = meet r l
167+ meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
168− meetSemilatticeJoinIsIdempotent : (e : a) -> meet e e = e
168+ meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
170-- Sets equipped with a binary operation that is commutative, associative and
170-- Sets equipped with a binary operation that is commutative, associative and
171-- idempotent and supplied with a neutral element. Must satisfy the following
171-- idempotent and supplied with a neutral element. Must satisfy the following