PosetFactory(S)

logic.spad line 2119 [edit on github]

• S : SetCategory

Provides functions to construct various small posets including powerset. Perhaps it should be called a 'powerlist' but since we do not expect duplicates or require 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.