1 files changed, 57 insertions, 0 deletions
diff --git a/std/Unary.bruijn b/std/Unary.bruijn
new file mode 100644
index 0000000..cf72e3b
--- /dev/null
+++ b/std/Unary.bruijn
@@ -0,0 +1,57 @@
+# MIT License, Copyright (c) 2022 Marvin Borner
+# classic Church style numerals
+
+:import std/Logic .
+
+zero [[0]]
+
+# returns true if a unary number is zero
+zero? [0 [[[0]]] [[1]]] ⧗ Unary → Boolean
+
+=?‣ zero?
+
+:test (=?(+0u)) (true)
+:test (=?(+42u)) (false)
+
+# adds 1 to a unary number
+inc [[[1 (2 1 0)]]] ⧗ Unary → Unary
+
+++‣ inc
+
+:test (++(+0u)) ((+1u))
+:test (++(+1u)) ((+2u))
+:test (++(+42u)) ((+43u))
+
+# subs 1 from a unary number
+dec [[[2 [[0 (1 3)]] [1] [0]]]] ⧗ Unary → Unary
+
+--‣ dec
+
+:test (--(+0u)) ((+0u))
+:test (--(+1u)) ((+0u))
+:test (--(+42u)) ((+41u))
+
+# adds two unary numbers
+add [[[[3 1 (2 1 0)]]]] ⧗ Unary → Unary → Unary
+
+…+… add
+
+:test ((+0u) + (+2u)) ((+2u))
+:test ((+5u) + (+3u)) ((+8u))
+
+# muls two unary numbers
+mul [[[2 (1 0)]]] ⧗ Unary → Unary → Unary
+
+…⋅… mul
+
+:test ((+0u) ⋅ (+2u)) ((+0u))
+:test ((+2u) ⋅ (+3u)) ((+6u))
+
+# exponentiates two unary numbers
+# gives 1 if exponent is 0
+exp [[0 1]] ⧗ Unary → Unary → Unary
+
+…^… exp
+
+:test ((+1u) ^ (+0u)) ((+1u))
+:test ((+2u) ^ (+3u)) ((+8u))