git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/iif/adder.iif
30 lines 681 B history raw
1data O 0
2data S 1
4fun plus(x, y) = case x of {
5 O => y
6 | S(k) => S (plus(k, y))
7 }
9fun natToInt(x) = case x of {
10 O => 0
11 | S(k) => let y = natToInt(k) in y + 1
12 }
14fun adder(arity, acc) = case arity of {
15 O => acc
16 | S(k) => adderAux(k, acc)
17 }
19fun adderAux(k, acc, n) = adder(k, plus(acc, n))
21fun zero() = O
22fun one() = S(zero)
23fun two() = S(one)
24fun three() = S(two)
25fun four() = S(three)
26fun five() = S(four)
28fun main() = %WriteInt(natToInt(adder(three, two, three, four, five)))