mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-22 22:47:12 +03:00
20 lines
463 B
Plaintext
20 lines
463 B
Plaintext
data O 0
|
|
data S 1
|
|
|
|
fun plus(x, y) = case x of {
|
|
O => y
|
|
| S(k) => S (plus(k, y))
|
|
}
|
|
|
|
fun natToInt(x) = case x of {
|
|
O => 0
|
|
| S(k) => let y = natToInt(k) in y + 1
|
|
}
|
|
|
|
fun intToNat(x) = case x of {
|
|
0 => O
|
|
| _ => S (intToNat (x - 1))
|
|
}
|
|
|
|
fun main() = printNum(natToInt(plus(S(S(O)), intToNat(2))))
|