std/Number/Bruijn.bruijn


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30

# MIT License, Copyright (c) 2023 Marvin Borner
# de Bruijn numeral system (named by me)
# proof that this numeral system does not support zero/eq/sub/etc. is in
#   Wadsworth, Christopher. "Some unusual λ-calculus numeral systems."
# very sad indeed

# increments de Bruijn numeral
inc [[[2 1]]] ⧗ Bruijn → Bruijn

++‣ inc

:test (++(+0d)) ((+1d))
:test (++(+5d)) ((+6d))

# decrements de Bruijn numeral
dec [[1 0 0]] ⧗ Bruijn → Bruijn

--‣ dec

:test (--(+1d)) ((+0d))
:test (--(+5d)) ((+4d))

# multiplies de Bruijn numeral with unary number
mul [[1 0]] ⧗ Unary → Bruijn → Bruijn

…⋅… mul

:test ((+5u) ⋅ (+5d)) ((+25d))
:test ((+0u) ⋅ (+5d)) ((+0d))
:test ((+5u) ⋅ (+0d)) ((+0d))