Number/Parigot.bruijn

# MIT License, Copyright (c) 2024 Marvin Borner
# see "on the representation of data in lambda-calculus" (Parigot 1989)
# has a "one-step" predecessor *and* addition function

# zero Parigot number
zero [0] ⧗ Parigot

# increments Parigot number
inc [[[0 (2 1)]]] ⧗ Parigot → Parigot

++‣ inc

# decrements Parigot number
dec [[1 0 [0]]] ⧗ Parigot → Parigot

--‣ dec

:test (dec (inc zero)) (zero)

# adds two Parigot numbers
add [[[2 (1 0)]]] ⧗ Parigot → Parigot → Parigot

…+… add

:test (add (inc (zero)) (inc (inc zero))) (inc (inc (inc zero)))

iter [[[0 ι ρ ρ]]]
	ρ [[3 (1 0 0)]]
	ι [[4]]

rec [[[0 ι ρ ρ --0]]]
	ρ [[[4 0 (2 1 1)]]]
	ι [[[5]]]