UserDefinedPartialOrdering(S)

setorder.spad line 1 [edit on github]

• S : SetCategory

Provides functions to force a partial ordering on any set.

getOrder : () -> Record(low : List(S), high : List(S))

getOrder() returns [[b1, ..., bm], [a1, ..., an]] such that the partial ordering on S was given by setOrder([b1, ..., bm], [a1, ..., an]).

largest : List(S) -> S if S has OrderedSet

largest l returns the largest element of l where the partial ordering induced by setOrder is completed into a total one by the ordering on S.

largest : (List(S), Mapping(Boolean, S, S)) -> S

largest(l, fn) returns the largest element of l where the partial ordering induced by setOrder is completed into a total one by fn.

less? : (S, S, Mapping(Boolean, S, S)) -> Boolean

less?(a, b, fn) compares a and b in the partial ordering induced by setOrder, and returns fn(a, b) if a and b are not comparable in that ordering.

less? : (S, S) -> Union(Boolean, "failed")

less?(a, b) compares a and b in the partial ordering induced by setOrder.

more? : (S, S) -> Boolean if S has OrderedSet

more?(a, b) compares a and b in the partial ordering induced by setOrder, and uses the ordering on S if a and b are not comparable in the partial ordering.

setOrder : List(S) -> Void

setOrder([a1, ..., an]) defines a partial ordering on S given by: (1)a1 < a2 < ... < an. (2)b < aifor i = 1..n and b not among the ai's. (3)undefined on (b, c) if neither is among the ai's.

setOrder : (List(S), List(S)) -> Void

setOrder([b1, ..., bm], [a1, ..., an]) defines a partial ordering on S given by: (1)b1 < b2 < ... < bm < a1 < a2 < ... < an. (2)bj < c < aifor c not among the ai's and bj's. (3)undefined on (c, d) if neither is among the ai's, bj's.

userOrdered? : () -> Boolean

userOrdered?() tests if the partial ordering induced by setOrder is not empty.