PosetFactory S

logic.spad line 2123 [edit on github]

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.