PosetFactory SΒΆ

logic.spad line 2251

Provides functions to construct various small posets including powerset. Perhaps it should be called a ‘powerlist’ but since we do not expect duplicates or reqire specific ordering it is essentially the same.

completelyOrderedSet: List S -> FiniteBiCPO S
generates a completely ordered set
posetL7: List S -> FiniteBiCPO S
generates a poset corresponding to an L7 lattice
posetM5: List S -> FiniteBiCPO S
generates a poset corresponding to an M5 lattice
posetN5: List S -> FiniteBiCPO S
generates a poset corresponding to an N5 lattice
posetO6: List S -> FiniteBiCPO S
generates a poset corresponding to an O6 lattice
posetP6: List S -> FiniteBiCPO S
generates a poset corresponding to an P6 lattice
powerset: List S -> FiniteBiCPO List S
generate a poset representing all possible subsets of a given set with their subset relationships.