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

   1 :load Bool.cloe
   2
   3 Eq_Equal
   4  (X:*)
   5  = X -> X -> Bool
   6
   7 Eq_Class
   8  (X:*) (Data:*)
   9  = (equal:Eq_Equal X)
  10  -> Data
  11 Eq_Polytype
  12  (X:*) : *p
  13  = (Data:*) -> Eq_Class X Data -> Data
  14 Eq
  15  (X:*) : *m
  16  = Monotype (Eq_Polytype X)
  17
  18 eq
  19  (X:*)
  20  (equal:Eq_Equal X)
  21  : Eq X
  22  = monotype (Eq_Polytype X)
  23      (λ(Data:*) (eq_class:Eq_Class X Data) -> eq_class equal)
  24 unEq
  25  (X:*) (Data:*)
  26  (eq_class:Eq_Class X Data)
  27  (eq:Eq X)
  28  : Data
  29  = polytype (Eq_Polytype X) eq Data eq_class
  30
  31 Eq_equal
  32  (X:*) (eq:Eq X)
  33  : Eq_Equal X
  34  = unEq X (Eq_Equal X)
  35     (λ(equal:Eq_Equal X) -> equal)
  36     eq