package preface

A Join_semilattice capture the notion of a set with least upper bound with a bottom . A bounded join semilattice is an idempotent commutative semigroup.

Laws

To have a predictable behaviour, the instance of Bounded_join_semilattice must obey some laws.

• join a (join b c) = join (join a b) c
• join a b = join b a
• join a a = a
• join a bottom = a

Minimal definition

Structure anatomy

Complete API