data Nat : Type where Z : Nat S : Nat -> NatAdderTy : Nat -> TypeAdderTy Z = NatAdderTy (S $k) = Nat -> AdderTy kplus : Nat -> Nat -> Natplus Z $y = yplus (S $k) $y = S (plus k y)adder : (i : Nat) -> (acc : Nat) -> AdderTy iadder Z $acc = accadder (S $k) $acc = \x => adder k (plus x acc)
data Nat : Type where
Z : Nat
S : Nat -> Nat
AdderTy : Nat -> Type
AdderTy Z = Nat
AdderTy (S $k) = Nat -> AdderTy k
plus : Nat -> Nat -> Nat
plus Z $y = y
plus (S $k) $y = S (plus k y)
adder : (i : Nat) -> (acc : Nat) -> AdderTy i
adder Z $acc = acc
adder (S $k) $acc = \x => adder k (plus x acc)