FreeDistributiveLattice
class FreeDistributiveLattice<A> : HeytingAlgebra<FreeDistributiveLattice<A>>
Content copied to clipboard
The free distributive lattice over an arbitrary set A
of elements. In addition to lattice identities, the following hold:
a /\ (b \/ c) == (a /\ b) \/ (a /\ c)
a \/ (b /\ c) == (a \/ b) /\ (a \/ c)
Constructors
FreeDistributiveLattice
Link copied to clipboard
Types
Functions
imply
Link copied to clipboard
open override fun imply(that: FreeDistributiveLattice<A>): FreeDistributiveLattice<A>
Content copied to clipboard
Returns the relative pseudocomplement of this
relative to that
. the relative pseudocomplement is greatest x s.t. this & x <= that
.
join
Link copied to clipboard
open override fun join(that: FreeDistributiveLattice<A>): FreeDistributiveLattice<A>
Content copied to clipboard
The least upper bound of this
and that.
lessThanOrEqualTo
Link copied to clipboard
open override fun lessThanOrEqualTo(that: FreeDistributiveLattice<A>): Boolean
Content copied to clipboard
Returns true if this
is ordered before that.
meet
Link copied to clipboard
open override fun meet(that: FreeDistributiveLattice<A>): FreeDistributiveLattice<A>
Content copied to clipboard
The greatest lower bound of this
and that.