@@ -35,8 +35,8 @@ class Semigroup a => Monoid a where
3535 neutral : a
3636
3737class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
38− monoidIsNeutralL : (l : a) -> l <+> neutral = l
39− monoidIsNeutralR : (r : a) -> neutral <+> r = r
38+ monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l
39+ monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r
4040
4141-- Sets equipped with a single binary operation that is associative, along with
4242-- a neutral element for that binary operation and inverses for all elements.
@@ -100,9 +100,9 @@ class AbelianGroup a => Ring a where
100100 (<*>) : a -> a -> a
101101
102102class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where
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)
105− ringOpsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)
103+ ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
104+ ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)
105+ ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <*> r = (l <*> r) <+> (l <*> c)
106106
107107-- Sets equipped with two binary operations, one associative and commutative
108108-- supplied with a neutral element, and the other associative supplied with a
@@ -163,9 +163,9 @@ class MeetSemilattice a where
163163 meet : a -> a -> a
164164
165165class MeetSemilattice a => VerifiedMeetSemilattice a where
166− meetSemilatticeJoinIsAssociative : (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
168− meetSemilatticeJoinIsIdempotent : (e : a) -> meet e e = e
166+ meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
167+ meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
168+ meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
169169
170170-- Sets equipped with a binary operation that is commutative, associative and
171171-- idempotent and supplied with a neutral element. Must satisfy the following