# MIT License, Copyright (c) 2024 Marvin Borner
# see "on the representation of data in lambda-calculus" #5
# has a "one-step" predecessor *and* addition function
# has 2x space complexity compared to unary/Church
zero [0]
inc [[[0 2 1]]]
++‣ inc
dec [[1 0 [0]]]
--‣ dec
:test (dec (inc zero)) (zero)
iter [[[0 ι ρ ρ]]]
ρ [[3 (1 0 0)]]
ι [[4]]
rec [[[0 ι ρ ρ --0]]]
ρ [[[4 0 (2 1 1)]]]
ι [[[5]]]