calculus/Calculus/Lambda/Omega/Explicit/lib/Ord.cloe

   1 Ordering_Polytype : *p
   2  = (Data:*) -> (Lt:Data) -> (Eq:Data) -> (Gt:Data) -> Data
   3 Ordering : *m = Monotype Ordering_Polytype
   4
   5 Ord_Lt : Ordering = monotype Ordering_Polytype (λ(Data:*) (Lt:Data) (Eq:Data) (Gt:Data) -> Lt)
   6 Ord_Eq : Ordering = monotype Ordering_Polytype (λ(Data:*) (Lt:Data) (Eq:Data) (Gt:Data) -> Eq)
   7 Ord_Gt : Ordering = monotype Ordering_Polytype (λ(Data:*) (Lt:Data) (Eq:Data) (Gt:Data) -> Gt)
   8
   9 :load Eq.cloe
  10
  11 Ord_Compare (X:*) = X -> X -> Ordering
  12
  13 Ord_Class
  14  (X:*) (Data:*)
  15  =  (eq:Eq X)
  16  -> (compare:Ord_Compare X)
  17  -> Data
  18 Ord_Polytype
  19  (X:*) : *p
  20  = (Data:*) -> Ord_Class X Data -> Data
  21 Ord
  22  (X:*) : *m
  23  = Monotype (Ord_Polytype X)
  24
  25 ord
  26  (X:*)
  27  (eq:Eq X)
  28  (compare:Ord_Compare X)
  29  : Ord X
  30  = monotype (Ord_Polytype X)
  31     (λ(Data:*) (ord_class:Ord_Class X Data) ->
  32       ord_class eq compare)
  33 unOrd
  34  (X:*) (Data:*)
  35  (ord_class:Ord_Class X Data)
  36  (ord:Ord X)
  37  : Data
  38  = polytype (Ord_Polytype X) ord Data ord_class
  39
  40 Ord_eq
  41  (X:*) (ord:Ord X)
  42  : Eq X
  43  = unOrd X (Eq X)
  44     (λ(eq:Eq X) (compare:Ord_Compare X) -> eq)
  45     ord
  46 Ord_compare
  47  (X:*) (ord:Ord X)
  48  : Ord_Compare X
  49  = unOrd X (Ord_Compare X)
  50     (λ(eq:Eq X) (compare:Ord_Compare X) -> compare)
  51     ord