@@ -187,7 +187,7 @@ class MeetSemilattice a => VerifiedMeetSemilattice a where
187||| + Idempotency of join:
187||| + Idempotency of join:
188||| forall a, join a a == a
188||| forall a, join a a == a
189||| + Bottom:
189||| + Bottom:
190−||| forall a, join a bottom == bottom
190+||| forall a, join a bottom == a
192||| Join semilattices capture the notion of sets with a "least upper bound"
192||| Join semilattices capture the notion of sets with a "least upper bound"
193||| equipped with a "bottom" element.
193||| equipped with a "bottom" element.
@@ -195,7 +195,7 @@ class JoinSemilattice a => BoundedJoinSemilattice a where
195 bottom : a
195 bottom : a
197class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
197class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where
198− total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = bottom
198+ total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = e
200||| Sets equipped with a binary operation that is commutative, associative and
200||| Sets equipped with a binary operation that is commutative, associative and
201||| idempotent and supplied with a neutral element. Must satisfy the following
201||| idempotent and supplied with a neutral element. Must satisfy the following
@@ -208,7 +208,7 @@ class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJo
208||| + Idempotency of meet:
208||| + Idempotency of meet:
209||| forall a, meet a a == a
209||| forall a, meet a a == a
210||| + Top:
210||| + Top:
211−||| forall a, meet a top == top
211+||| forall a, meet a top == a
213||| Meet semilattices capture the notion of sets with a "greatest lower bound"
213||| Meet semilattices capture the notion of sets with a "greatest lower bound"
214||| equipped with a "top" element.
214||| equipped with a "top" element.
@@ -216,7 +216,7 @@ class MeetSemilattice a => BoundedMeetSemilattice a where
218class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
218class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where
219− total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = top
219+ total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e top = e
221||| Sets equipped with two binary operations that are both commutative,
221||| Sets equipped with two binary operations that are both commutative,
222||| associative and idempotent, along with absorbtion laws for relating the two
222||| associative and idempotent, along with absorbtion laws for relating the two