git.iko.soy/Idris-dev
on master help sign in
Clarify semilattice documentation
5b37733Sam Elliott
libs/prelude/Prelude/Algebra.idr+4−4
compare with master
unifiedsplit
@@ -177,7 +177,7 @@ class MeetSemilattice a => VerifiedMeetSemilattice a where
177 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
177 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e
178
178
179||| Sets equipped with a binary operation that is commutative, associative and
179||| Sets equipped with a binary operation that is commutative, associative and
180−||| idempotent and supplied with a neutral element. Must satisfy the following
180+||| idempotent and supplied with a unitary element. Must satisfy the following
181||| laws:
181||| laws:
182|||
182|||
183||| + Associativity of join:
183||| + Associativity of join:
@@ -186,7 +186,7 @@ class MeetSemilattice a => VerifiedMeetSemilattice a where
186||| forall a b, join a b == join b a
186||| forall a b, join a b == join b a
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 (Unitary Element):
190||| forall a, join a bottom == a
190||| forall a, join a bottom == a
191|||
191|||
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"
@@ -198,7 +198,7 @@ class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJo
198 total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = e
198 total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e bottom = e
199
199
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 unitary element. Must satisfy the following
202||| laws:
202||| laws:
203|||
203|||
204||| + Associativity of meet:
204||| + Associativity of meet:
@@ -207,7 +207,7 @@ class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJo
207||| forall a b, meet a b == meet b a
207||| forall a b, meet a b == meet b a
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 (Unitary Element):
211||| forall a, meet a top == a
211||| forall a, meet a top == a
212|||
212|||
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"