1	import Base
2	
3	# Total-order laws for a static comparator ~cmp : A -> A -> Cmp, the
4	# precondition every ordered container states its contract under.
5	#   flip:    cmp(b, a) = flip(cmp(a, b))
6	#   antisym: cmp(a, b) = EQ  implies  a == b
7	#   trans:   a <= b and b <= c  implies  a <= c     (<= is cmp in {LT, EQ})
8	# The lemmas and the U32 / String instances are in proofs/lib/order.bend.
9	
10	def flipc(c: Cmp) -> Cmp:
11	  match c:
12	    case LT{}:
13	      GT{}
14	    case EQ{}:
15	      EQ{}
16	    case GT{}:
17	      LT{}
18	
19	def Order(~A: Data, ~cmp: A -> A -> Cmp) -> Type:
20	  (@+a: A -> @+b: A -> {cmp(b, a) == flipc(cmp(a, b)) : Cmp}) & ((@+a: A -> @+b: A -> @+e: {cmp(a, b) == EQ{} : Cmp} -> {a == b : A}) & (@+a: A -> @+b: A -> @+c: A -> @+ab: {Cmp.is_le(cmp(a, b)) == True{} : Bool} -> @+bc: {Cmp.is_le(cmp(b, c)) == True{} : Bool} -> {Cmp.is_le(cmp(a, c)) == True{} : Bool}))