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

   1 Pair_Polytype (X:*) (Y:*) : *p = (Data:*) -> (X -> Y -> Data) -> Data
   2 Pair  (X:*) (Y:*) : *m = Monotype (Pair_Polytype X Y)
   3 pair (X:*) (Y:*) (x:X) (y:Y) : Pair X Y
   4  = monotype (Pair_Polytype X Y)
   5    (λ(Data:*) (f:X -> Y -> Data) -> f x y)
   6
   7 uncurry (X:*) (Y:*) (Data:*) (r:X -> Y -> Data) (p:Pair X Y) : Data
   8  = polytype (Pair_Polytype X Y)
   9    p Data r
  10 curry (X:*) (Y:*) (Data:*) (r:Pair X Y -> Data) (x:X) (y:Y)
  11  = r (pair X Y x y)
  12
  13 fst (X:*) (Y:*) (p:Pair X Y) : X
  14  = uncurry X Y X (λ(x:X) (y:Y) -> x) p
  15 snd (X:*) (Y:*) (p:Pair X Y) : Y
  16  = uncurry X Y Y (λ(x:X) (y:Y) -> y) p
  17 repair (X:*) (Y:*) (p:Pair X Y) : Pair X Y
  18  = pair X Y (fst X Y p) (snd X Y p)
  19
  20 first (X:*) (Y:*) (Z:*) (f:X -> Z) (p:Pair X Y) : Pair Z Y
  21  = uncurry X Y (Pair Z Y) (λ(x:X) (y:Y) -> pair Z Y (f x) y) p
  22 second (X:*) (Y:*) (Z:*) (f:Y -> Z) (p:Pair X Y) : Pair X Z
  23  = uncurry X Y (Pair X Z) (λ(x:X) (y:Y) -> pair X Z x (f y)) p