@@ -21,7 +21,7 @@ class Semigroup a where
2121 (<+>) : a -> a -> a
2222
2323class Semigroup a => VerifiedSemigroup a where
24− semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
24+ total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r
2525
2626-- Sets equipped with a single binary operation that is associative, along with
2727-- a neutral element for that binary operation. Must satisfy the following
@@ -35,8 +35,8 @@ class Semigroup a => Monoid a where
3535 neutral : a
3636
3737class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where
38− monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l
39− monoidNeutralIsNeutralR : (r : a) -> neutral <+> r = r
38+ total monoidNeutralIsNeutralL : (l : a) -> l <+> neutral = l
39+ total 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.
@@ -53,8 +53,8 @@ class Monoid a => Group a where
5353 inverse : a -> a
5454
5555class (VerifiedMonoid a, Group a) => VerifiedGroup a where
56− groupInverseIsInverseL : (l : a) -> l <+> inverse l = neutral
57− groupInverseIsInverseR : (r : a) -> inverse r <+> r = neutral
56+ total groupInverseIsInverseL : (l : a) -> l <+> inverse l = neutral
57+ total groupInverseIsInverseR : (r : a) -> inverse r <+> r = neutral
5858
5959(<->) : Group a => a -> a -> a
6060(<->) left right = left <+> (inverse right)
@@ -75,7 +75,7 @@ class (VerifiedMonoid a, Group a) => VerifiedGroup a where
7575class Group a => AbelianGroup a where { }
7676
7777class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where
78− abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
78+ total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l
7979
8080-- Sets equipped with two binary operations, one associative and commutative
8181-- supplied with a neutral element, and the other associative, with
@@ -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− 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)
103+ total ringOpIsAssociative : (l, c, r : a) -> l <*> (c <*> r) = (l <*> c) <*> r
104+ total ringOpIsDistributiveL : (l, c, r : a) -> l <*> (c <+> r) = (l <*> c) <+> (l <*> r)
105+ total 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
@@ -130,8 +130,8 @@ class Ring a => RingWithUnity a where
130130 unity : a
131131
132132class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where
133− ringWithUnityIsUnityL : (l : a) -> l <*> unity = l
134− ringWithUnityIsUnityR : (r : a) -> unity <*> r = r
133+ total ringWithUnityIsUnityL : (l : a) -> l <*> unity = l
134+ total ringWithUnityIsUnityR : (r : a) -> unity <*> r = r
135135
136136-- Sets equipped with a binary operation that is commutative, associative and
137137-- idempotent. Must satisfy the following laws:
@@ -146,9 +146,9 @@ class JoinSemilattice a where
146146 join : a -> a -> a
147147
148148class JoinSemilattice a => VerifiedJoinSemilattice a where
149− joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
150− joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l
151− joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e
149+ total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r
150+ total joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l
151+ total joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e
152152
153153-- Sets equipped with a binary operation that is commutative, associative and
154154-- idempotent. Must satisfy the following laws:
@@ -163,9 +163,9 @@ class MeetSemilattice a where
163163 meet : a -> a -> a
164164
165165class MeetSemilattice a => VerifiedMeetSemilattice a where
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
166+ total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r
167+ total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l
168+ total 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
@@ -184,7 +184,7 @@ class JoinSemilattice a => BoundedJoinSemilattice a where
184184 bottom : a
185185
186186class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
187− boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom
187+ total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom
188188
189189-- Sets equipped with a binary operation that is commutative, associative and
190190-- idempotent and supplied with a neutral element. Must satisfy the following
@@ -203,7 +203,7 @@ class MeetSemilattice a => BoundedMeetSemilattice a where
203203 top : a
204204
205205class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
206− boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top
206+ total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top
207207
208208-- Sets equipped with two binary operations that are both commutative,
209209-- associative and idempotent, along with absorbtion laws for relating the two
@@ -223,8 +223,8 @@ class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMe
223223class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }
224224
225225class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where
226− latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l
227− latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l
226+ total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l
227+ total latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l
228228
229229-- Sets equipped with two binary operations that are both commutative,
230230-- associative and idempotent and supplied with neutral elements, along with