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

   1 Nat_Polytype : *p
   2  = (Data:*) -> (Succ:Data -> Data) -> (Zero:Data) -> Data
   3 Nat : *m  = Monotype Nat_Polytype
   4 zero : Nat = (monotype Nat_Polytype) (λ(Data:*) (Succ:Data -> Data) (Zero:Data) -> Zero)
   5 succ (n:Nat) : Nat
   6  = monotype Nat_Polytype
   7    (λ(Data:*) (Succ:Data -> Data) (Zero:Data) ->
   8      Succ (polytype Nat_Polytype n Data Succ Zero))
   9 one   : Nat = succ zero
  10 two   : Nat = succ one
  11 three : Nat = succ two
  12 plus (n:Nat) (m:Nat) : Nat
  13  = monotype Nat_Polytype
  14    (λ(Data:*) (Succ:Data -> Data) (Zero:Data) ->
  15      polytype Nat_Polytype n Data Succ (polytype Nat_Polytype m Data Succ Zero))
  16 mult (n:Nat) (m:Nat) : Nat
  17  = monotype Nat_Polytype
  18    (λ(Data:*) (Succ:Data -> Data) (Zero:Data) ->
  19      polytype Nat_Polytype n Data (polytype Nat_Polytype m Data Succ) Zero)