Unicodification

I like unicode, sorry if you have a different opinion

6 files changed, 446 insertions, 289 deletions

diff --git a/editors/vim/bruijn.snippets b/editors/vim/bruijn.snippets
index 35b94cf..f0bd285 100644
--- a/editors/vim/bruijn.snippets
+++ b/editors/vim/bruijn.snippets
@@ -1,213 +1,374 @@
+# MIT License, Copyright (c) 2022 Marvin Borner
+# don't worry, this is mostly automatically generated
+
 priority 0
 
 # === Definition snippets === 
 
-snippet "(.+)>" "prefix" r
+snippet "(.+)>" "" r
 `!p snip.rv = match.group(1)`‣ $0
 endsnippet
 
-snippet "(.*)\." "mixfix" r
+snippet "(.*)\." "" r
 `!p snip.rv = match.group(1)`…$0
 endsnippet
 
+# === Operators ===
+
+snippet "(.*)&&" "" r
+`!p snip.rv = match.group(1)`⋀$0
+endsnippet
+
+snippet "(.*)\|\|" "" r
+`!p snip.rv = match.group(1)`⋁$0
+endsnippet
+
+snippet "(.*)=>" "" r
+`!p snip.rv = match.group(1)`⇒$0
+endsnippet
+
+snippet "(.*)<=>" "" r
+`!p snip.rv = match.group(1)`⇔$0
+endsnippet
+
+snippet "(.*)->" "" r
+`!p snip.rv = match.group(1)`→$0
+endsnippet
+
+snippet "(.*)<->" "" r
+`!p snip.rv = match.group(1)`↔$0
+endsnippet
+
+snippet "(.*)<=" "" r
+`!p snip.rv = match.group(1)`≤$0
+endsnippet
+
+snippet "(.*)>=" "" r
+`!p snip.rv = match.group(1)`≥$0
+endsnippet
+
+snippet "(.*)!" "" r
+`!p snip.rv = match.group(1)`¬$0
+endsnippet
+
+snippet "(.*)_0" "" r
+`!p snip.rv = match.group(1)`₀$0
+endsnippet
+
+snippet "(.*)_1" "" r
+`!p snip.rv = match.group(1)`₁$0
+endsnippet
+
+snippet "(.*)_2" "" r
+`!p snip.rv = match.group(1)`₂$0
+endsnippet
+
+snippet "(.*)_3" "" r
+`!p snip.rv = match.group(1)`₃$0
+endsnippet
+
+snippet "(.*)_4" "" r
+`!p snip.rv = match.group(1)`₄$0
+endsnippet
+
+snippet "(.*)_5" "" r
+`!p snip.rv = match.group(1)`₅$0
+endsnippet
+
+snippet "(.*)_6" "" r
+`!p snip.rv = match.group(1)`₆$0
+endsnippet
+
+snippet "(.*)_7" "" r
+`!p snip.rv = match.group(1)`₇$0
+endsnippet
+
+snippet "(.*)_8" "" r
+`!p snip.rv = match.group(1)`₈$0
+endsnippet
+
+snippet "(.*)_9" "" r
+`!p snip.rv = match.group(1)`₉$0
+endsnippet
+
+snippet "(.*)_+" "" r
+`!p snip.rv = match.group(1)`₊$0
+endsnippet
+
+snippet "(.*)_-" "" r
+`!p snip.rv = match.group(1)`₋$0
+endsnippet
+
+snippet "(.*)_=" "" r
+`!p snip.rv = match.group(1)`₌$0
+endsnippet
+
+snippet "(.*)_\(" "" r
+`!p snip.rv = match.group(1)`₍$0
+endsnippet
+
+snippet "(.*)_\)" "" r
+`!p snip.rv = match.group(1)`₎$0
+endsnippet
+
+snippet "(.*)\^0" "" r
+`!p snip.rv = match.group(1)`⁰$0
+endsnippet
+
+snippet "(.*)\^1" "" r
+`!p snip.rv = match.group(1)`¹$0
+endsnippet
+
+snippet "(.*)\^2" "" r
+`!p snip.rv = match.group(1)`²$0
+endsnippet
+
+snippet "(.*)\^3" "" r
+`!p snip.rv = match.group(1)`³$0
+endsnippet
+
+snippet "(.*)\^4" "" r
+`!p snip.rv = match.group(1)`⁴$0
+endsnippet
+
+snippet "(.*)\^5" "" r
+`!p snip.rv = match.group(1)`⁵$0
+endsnippet
+
+snippet "(.*)\^6" "" r
+`!p snip.rv = match.group(1)`⁶$0
+endsnippet
+
+snippet "(.*)\^7" "" r
+`!p snip.rv = match.group(1)`⁷$0
+endsnippet
+
+snippet "(.*)\^8" "" r
+`!p snip.rv = match.group(1)`⁸$0
+endsnippet
+
+snippet "(.*)\^9" "" r
+`!p snip.rv = match.group(1)`⁹$0
+endsnippet
+
+snippet "(.*)\^+" "" r
+`!p snip.rv = match.group(1)`⁺$0
+endsnippet
+
+snippet "(.*)\^-" "" r
+`!p snip.rv = match.group(1)`⁻$0
+endsnippet
+
+snippet "(.*)\^=" "" r
+`!p snip.rv = match.group(1)`⁼$0
+endsnippet
+
+snippet "(.*)\^\(" "" r
+`!p snip.rv = match.group(1)`⁽$0
+endsnippet
+
+snippet "(.*)\^\)" "" r
+`!p snip.rv = match.group(1)`⁾$0
+endsnippet
+
 # === Greek letters === 
 
-snippet Alpha
-Α
+snippet "(.*)Alpha" "" r
+`!p snip.rv = match.group(1)`Α$0
 endsnippet
 
-snippet alpha
-α
+snippet "(.*)alpha" "" r
+`!p snip.rv = match.group(1)`α$0
 endsnippet
 
-snippet Beta
-Β
+snippet "(.*)Beta" "" r
+`!p snip.rv = match.group(1)`Β$0
 endsnippet
 
-snippet beta
-β
+snippet "(.*)beta" "" r
+`!p snip.rv = match.group(1)`β$0
 endsnippet
 
-snippet Gamma
-Γ
+snippet "(.*)Gamma" "" r
+`!p snip.rv = match.group(1)`Γ$0
 endsnippet
 
-snippet gamma
-γ
+snippet "(.*)gamma" "" r
+`!p snip.rv = match.group(1)`γ$0
 endsnippet
 
-snippet Delta
-Δ
+snippet "(.*)Delta" "" r
+`!p snip.rv = match.group(1)`Δ$0
 endsnippet
 
-snippet delta
-δ
+snippet "(.*)delta" "" r
+`!p snip.rv = match.group(1)`δ$0
 endsnippet
 
-snippet Epsilon
-Ε
+snippet "(.*)Epsilon" "" r
+`!p snip.rv = match.group(1)`Ε$0
 endsnippet
 
-snippet epsilon
-ε
+snippet "(.*)epsilon" "" r
+`!p snip.rv = match.group(1)`ε$0
 endsnippet
 
-snippet varepsilon
-ϵ
+snippet "(.*)varepsilon" "" r
+`!p snip.rv = match.group(1)`ϵ$0
 endsnippet
 
-snippet Zeta
-Ζ
+snippet "(.*)Zeta" "" r
+`!p snip.rv = match.group(1)`Ζ$0
 endsnippet
 
-snippet zeta
-ζ
+snippet "(.*)zeta" "" r
+`!p snip.rv = match.group(1)`ζ$0
 endsnippet
 
-snippet Eta
-Η
+snippet "(.*)Eta" "" r
+`!p snip.rv = match.group(1)`Η$0
 endsnippet
 
-snippet eta
-η
+snippet "(.*)eta" "" r
+`!p snip.rv = match.group(1)`η$0
 endsnippet
 
-snippet Theta
-Θ
+snippet "(.*)Theta" "" r
+`!p snip.rv = match.group(1)`Θ$0
 endsnippet
 
-snippet theta
-θ
+snippet "(.*)theta" "" r
+`!p snip.rv = match.group(1)`θ$0
 endsnippet
 
-snippet Iota
-Ι
+snippet "(.*)Iota" "" r
+`!p snip.rv = match.group(1)`Ι$0
 endsnippet
 
-snippet iota
-ι
+snippet "(.*)iota" "" r
+`!p snip.rv = match.group(1)`ι$0
 endsnippet
 
-snippet Kappa
-Κ
+snippet "(.*)Kappa" "" r
+`!p snip.rv = match.group(1)`Κ$0
 endsnippet
 
-snippet kappa
-κ
+snippet "(.*)kappa" "" r
+`!p snip.rv = match.group(1)`κ$0
 endsnippet
 
-snippet Lambda
-Λ
+snippet "(.*)Lambda" "" r
+`!p snip.rv = match.group(1)`Λ$0
 endsnippet
 
-snippet lambda
-λ
+snippet "(.*)lambda" "" r
+`!p snip.rv = match.group(1)`λ$0
 endsnippet
 
-snippet Mu
-Μ
+snippet "(.*)Mu" "" r
+`!p snip.rv = match.group(1)`Μ$0
 endsnippet
 
-snippet mu
-μ
+snippet "(.*)mu" "" r
+`!p snip.rv = match.group(1)`μ$0
 endsnippet
 
-snippet Nu
-Ν
+snippet "(.*)Nu" "" r
+`!p snip.rv = match.group(1)`Ν$0
 endsnippet
 
-snippet nu
-ν
+snippet "(.*)nu" "" r
+`!p snip.rv = match.group(1)`ν$0
 endsnippet
 
-snippet Xi
-Ξ
+snippet "(.*)Xi" "" r
+`!p snip.rv = match.group(1)`Ξ$0
 endsnippet
 
-snippet xi
-ξ
+snippet "(.*)xi" "" r
+`!p snip.rv = match.group(1)`ξ$0
 endsnippet
 
-snippet Omicron
-Ο
+snippet "(.*)Omicron" "" r
+`!p snip.rv = match.group(1)`Ο$0
 endsnippet
 
-snippet omicron
-ο
+snippet "(.*)omicron" "" r
+`!p snip.rv = match.group(1)`ο$0
 endsnippet
 
-snippet Pi
-Π
+snippet "(.*)Pi" "" r
+`!p snip.rv = match.group(1)`Π$0
 endsnippet
 
-snippet pi
-π
+snippet "(.*)pi" "" r
+`!p snip.rv = match.group(1)`π$0
 endsnippet
 
-snippet Rho
-Ρ
+snippet "(.*)Rho" "" r
+`!p snip.rv = match.group(1)`Ρ$0
 endsnippet
 
-snippet rho
-ρ
+snippet "(.*)rho" "" r
+`!p snip.rv = match.group(1)`ρ$0
 endsnippet
 
-snippet Sigma
-Σ
+snippet "(.*)Sigma" "" r
+`!p snip.rv = match.group(1)`Σ$0
 endsnippet
 
-snippet sigma
-σ
+snippet "(.*)sigma" "" r
+`!p snip.rv = match.group(1)`σ$0
 endsnippet
 
-snippet Tau
-Τ
+snippet "(.*)Tau" "" r
+`!p snip.rv = match.group(1)`Τ$0
 endsnippet
 
-snippet tau
-τ
+snippet "(.*)tau" "" r
+`!p snip.rv = match.group(1)`τ$0
 endsnippet
 
-snippet Upsilon
-Υ
+snippet "(.*)Upsilon" "" r
+`!p snip.rv = match.group(1)`Υ$0
 endsnippet
 
-snippet upsilon
-υ
+snippet "(.*)upsilon" "" r
+`!p snip.rv = match.group(1)`υ$0
 endsnippet
 
-snippet Phi
-Φ
+snippet "(.*)Phi" "" r
+`!p snip.rv = match.group(1)`Φ$0
 endsnippet
 
-snippet phi
-φ
+snippet "(.*)phi" "" r
+`!p snip.rv = match.group(1)`φ$0
 endsnippet
 
-snippet varphi
-ϕ
+snippet "(.*)varphi" "" r
+`!p snip.rv = match.group(1)`ϕ$0
 endsnippet
 
-snippet Chi
-Χ
+snippet "(.*)Chi" "" r
+`!p snip.rv = match.group(1)`Χ$0
 endsnippet
 
-snippet chi
-χ
+snippet "(.*)chi" "" r
+`!p snip.rv = match.group(1)`χ$0
 endsnippet
 
-snippet Psi
-Ψ
+snippet "(.*)Psi" "" r
+`!p snip.rv = match.group(1)`Ψ$0
 endsnippet
 
-snippet psi
-ψ
+snippet "(.*)psi" "" r
+`!p snip.rv = match.group(1)`ψ$0
 endsnippet
 
-snippet Omega
-Ω
+snippet "(.*)Omega" "" r
+`!p snip.rv = match.group(1)`Ω$0
 endsnippet
 
-snippet omega
-ω
+snippet "(.*)omega" "" r
+`!p snip.rv = match.group(1)`ω$0
 endsnippet
diff --git a/src/Parser.hs b/src/Parser.hs
index 15400f6..1952cde 100644
--- a/src/Parser.hs
+++ b/src/Parser.hs
@@ -17,10 +17,6 @@ type Parser = Parsec Void String
 sc :: Parser ()
 sc = void $ char ' '
 
--- "'" can't be in special chars because of 'c' char notation and prefixation
-specialChar :: Parser Char
-specialChar = oneOf "!?*@.,:;+-_#$%^&<>/\\|{}~="
-
 -- lower or upper
 greekLetter :: Parser Char
 greekLetter = satisfy isGreek
@@ -31,20 +27,26 @@ emoticon = satisfy isEmoticon
   where isEmoticon c = ('\128512' <= c && c <= '\128591')
 
 mathematicalOperator :: Parser Char
-mathematicalOperator = satisfy isMathematicalOperator
-  where isMathematicalOperator c = '∀' <= c && c <= '⋿'
+mathematicalOperator = satisfy isMathematicalUnicodeBlock
+  <|> oneOf "¬₀₁₂₃₄₅₆₇₈₉₊₋₌₍₎⁰¹²³⁴⁵⁶⁷⁸⁹⁺⁻⁼⁽⁾"
+  where isMathematicalUnicodeBlock c = ('∀' <= c && c <= '⋿')
 
 mathematicalArrow :: Parser Char
 mathematicalArrow = satisfy isMathematicalOperator
   where isMathematicalOperator c = '←' <= c && c <= '⇿'
 
+-- "'" can't be in special chars because of 'c' char notation and prefixation
+specialChar :: Parser Char
+specialChar =
+  oneOf "!?*@.,:;+-_#$%^&<>/\\|{}~="
+    <|> mathematicalOperator
+    <|> mathematicalArrow
+
 mixfixNone :: Parser MixfixIdentifierKind
 mixfixNone = char '…' >> pure MixfixNone
 
 mixfixSome :: Parser MixfixIdentifierKind
-mixfixSome =
-  MixfixSome
-    <$> (some $ specialChar <|> mathematicalOperator <|> mathematicalArrow)
+mixfixSome = MixfixSome <$> (some specialChar)
 
 mixfixOperator :: Parser Identifier
 mixfixOperator = normalMixfix <|> namespacedMixfix
@@ -55,8 +57,7 @@ mixfixOperator = normalMixfix <|> namespacedMixfix
 prefixOperator :: Parser Identifier
 prefixOperator = normalPrefix <|> namespacedPrefix
  where
-  normalPrefix = PrefixFunction
-    <$> some (specialChar <|> mathematicalOperator <|> mathematicalArrow)
+  normalPrefix     = PrefixFunction <$> some specialChar
   namespacedPrefix = NamespacedFunction <$> dottedNamespace <*> prefixOperator
 
 defIdentifier :: Parser Identifier
diff --git a/std/List.bruijn b/std/List.bruijn
index 1d43ecd..297f882 100644
--- a/std/List.bruijn
+++ b/std/List.bruijn
@@ -89,20 +89,20 @@ foldr1 [[foldl 1 ^0 ~0]]
 # applies or to all list elements
 lor? foldr or? false
 
-||‣ lor?
+⋁?‣ lor?
 
-:test (||(true : (true : empty))) (true)
-:test (||(true : (false : empty))) (true)
-:test (||(false : (false : empty))) (false)
+:test (⋁?(true : (true : empty))) (true)
+:test (⋁?(true : (false : empty))) (true)
+:test (⋁?(false : (false : empty))) (false)
 
 # applies and to all list elements
 land? foldr and? true
 
-&&‣ land?
+⋀?‣ land?
 
-:test (&&(true : (true : empty))) (true)
-:test (&&(true : (false : empty))) (false)
-:test (&&(false : (false : empty))) (false)
+:test (⋀?(true : (true : empty))) (true)
+:test (⋀?(true : (false : empty))) (false)
+:test (⋀?(false : (false : empty))) (false)
 
 # multiplies all values in list
 product foldl mul (+1)
@@ -141,8 +141,8 @@ list [0 [[[2 (0 : 1)]]] reverse empty]
 
 # appends two lists
 append z [[[rec]]]
-	rec <>?1 case-end case-merge
-		case-merge ^1 : (2 ~1 0)
+	rec <>?1 case-end case-append
+		case-append ^1 : (2 ~1 0)
 		case-end 0
 
 …++… append
@@ -263,21 +263,21 @@ span z [[[rec]]]
 			recced 2 1 ~0
 		case-end empty : empty
 
-:test (span (\(<?) (+3)) ((+1) : ((+2) : ((+4) : ((+1) : empty))))) (((+1) : ((+2) : empty)) : ((+4) : ((+1) : empty)))
+:test (span (\les? (+3)) ((+1) : ((+2) : ((+4) : ((+1) : empty))))) (((+1) : ((+2) : empty)) : ((+4) : ((+1) : empty)))
 
 # same as span but with inverted predicate
 break [span (not! . 0)]
 
-:test (break (\(>?) (+3)) ((+1) : ((+2) : ((+4) : ((+1) : empty))))) (((+1) : ((+2) : empty)) : ((+4) : ((+1) : empty)))
+:test (break (\gre? (+3)) ((+1) : ((+2) : ((+4) : ((+1) : empty))))) (((+1) : ((+2) : empty)) : ((+4) : ((+1) : empty)))
 
 # returns true if any element in a list matches a predicate
-any? [||‣ . (map 0)]
+any? [⋁?‣ . (map 0)]
 
 :test (any? (\gre? (+2)) ((+1) : ((+2) : ((+3) : empty)))) (true)
 :test (any? (\gre? (+2)) ((+1) : ((+2) : ((+2) : empty)))) (false)
 
 # returns true if all elements in a list match a predicate
-all? [&&‣ . (map 0)]
+all? [⋀?‣ . (map 0)]
 
 :test (all? (\gre? (+2)) ((+3) : ((+4) : ((+5) : empty)))) (true)
 :test (all? (\gre? (+2)) ((+4) : ((+3) : ((+2) : empty)))) (false)
@@ -285,15 +285,15 @@ all? [&&‣ . (map 0)]
 # returns true if element is part of a list based on eq predicate
 in? [[any? (\1 0)]]
 
-:test (in? (=?) (+3) ((+1) : ((+2) : ((+3) : empty)))) (true)
-:test (in? (=?) (+0) ((+1) : ((+2) : ((+3) : empty)))) (false)
+:test (in? …=?… (+3) ((+1) : ((+2) : ((+3) : empty)))) (true)
+:test (in? …=?… (+0) ((+1) : ((+2) : ((+3) : empty)))) (false)
 
 # returns true if all elements of one list are equal to corresponding elements of other list
-eq? &&‣ ... zip-with
+eq? ⋀?‣ ... zip-with
 
-:test (eq? (=?) ((+1) : ((+2) : empty)) ((+1) : ((+2) : empty))) (true)
-:test (eq? (=?) ((+1) : ((+2) : empty)) ((+2) : ((+2) : empty))) (false)
-:test (eq? (=?) empty empty) (true)
+:test (eq? …=?… ((+1) : ((+2) : empty)) ((+1) : ((+2) : empty))) (true)
+:test (eq? …=?… ((+1) : ((+2) : empty)) ((+2) : ((+2) : empty))) (false)
+:test (eq? …=?… empty empty) (true)
 
 # removes first element that match an eq predicate
 remove z [[[[rec]]]]
@@ -301,16 +301,16 @@ remove z [[[[rec]]]]
 		case-remove (2 ^0 1) ~0 (^0 : (3 2 1 ~0))
 		case-end empty
 
-:test (remove (=?) (+2) ((+1) : ((+2) : ((+3) : ((+2) : empty))))) ((+1) : ((+3) : ((+2) : empty)))
+:test (remove …=?… (+2) ((+1) : ((+2) : ((+3) : ((+2) : empty))))) ((+1) : ((+3) : ((+2) : empty)))
 
 # removes duplicates from list based on eq predicate (keeps first occurrence)
 nub z [[[rec]]]
 	rec <>?0 case-end case-nub
-		case-nub ^0 : (2 1 (~0 <#> [!(2 0 ^1)]))
+		case-nub ^0 : (2 1 (~0 <#> [¬(2 0 ^1)]))
 		case-end empty
 
-:test (nub (=?) ((+1) : ((+2) : ((+3) : empty)))) (((+1) : ((+2) : ((+3) : empty))))
-:test (nub (=?) ((+1) : ((+2) : ((+1) : empty)))) (((+1) : ((+2) : empty)))
+:test (nub …=?… ((+1) : ((+2) : ((+3) : empty)))) (((+1) : ((+2) : ((+3) : empty))))
+:test (nub …=?… ((+1) : ((+2) : ((+1) : empty)))) (((+1) : ((+2) : empty)))
 
 # returns a list with infinite-times a element
 repeat z [[rec]]
@@ -319,7 +319,7 @@ repeat z [[rec]]
 :test (take (+3) (repeat (+4))) ((+4) : ((+4) : ((+4) : empty)))
 
 # returns a list with n-times a element
-replicate [[take 1 (repeat 0)]]
+replicate \(g take repeat)
 
 :test (replicate (+3) (+4)) ((+4) : ((+4) : ((+4) : empty)))
 
diff --git a/std/Logic.bruijn b/std/Logic.bruijn
index e8127ab..06a08eb 100644
--- a/std/Logic.bruijn
+++ b/std/Logic.bruijn
@@ -9,22 +9,23 @@ true k
 false ki
 
 # inverts boolean value
+# equivalent of [0 ⇒ false]
 not! [0 false true]
 
-!‣ not!
+¬‣ not!
 
-:test (!true) (false)
-:test (!false) (true)
+:test (¬true) (false)
+:test (¬false) (true)
 
 # true if both args are true
 and? [[1 0 false]]
 
-…&&… and?
+…⋀?… and?
 
-:test (true && true) (true)
-:test (true && false) (false)
-:test (false && true) (false)
-:test (false && false) (false)
+:test (true ⋀? true) (true)
+:test (true ⋀? false) (false)
+:test (false ⋀? true) (false)
+:test (false ⋀? false) (false)
 
 # true if not both args are true
 nand? [[1 0 1 false true]]
@@ -37,12 +38,12 @@ nand? [[1 0 1 false true]]
 # true if one of the args is true
 or? [[1 true 0]]
 
-…||… or?
+…⋁?… or?
 
-:test (true || true) (true)
-:test (true || false) (true)
-:test (false || true) (true)
-:test (false || false) (false)
+:test (true ⋁? true) (true)
+:test (true ⋁? false) (true)
+:test (false ⋁? true) (true)
+:test (false ⋁? false) (false)
 
 # true if both args are false
 nor? [[1 1 0 false true]]
@@ -53,7 +54,7 @@ nor? [[1 1 0 false true]]
 :test (nor? false false) (true)
 
 # true if args are not same bools
-xor? [[1 !0 0]]
+xor? [[1 ¬0 0]]
 
 :test (xor? true true) (false)
 :test (xor? true false) (true)
@@ -61,7 +62,7 @@ xor? [[1 !0 0]]
 :test (xor? false false) (false)
 
 # true if both args are same bools
-xnor? [[1 0 !0]]
+xnor? [[1 0 ¬0]]
 
 :test (xnor? true true) (true)
 :test (xnor? true false) (false)
@@ -73,29 +74,29 @@ xnor? [[1 0 !0]]
 # I personally just write (exp? case-T case-F) directly
 if [[[2 1 0]]]
 
-…?!… if
+…?…:… if
 
 :test (if true true false) (true)
-:test ((true ?! true) false) (true)
+:test (true ? true : false) (true)
 :test (if false true false) (false)
-:test ((false ?! true) false) (false)
+:test (false ? true : false) (false)
 
 # mathematical implies definition
-implies [[!1 || 0]]
+implies [[¬1 ⋁? 0]]
 
-…=>?… implies
+…⇒?… implies
 
-:test (true =>? true) (true)
-:test (true =>? false) (false)
-:test (false =>? true) (true)
-:test (false =>? false) (true)
+:test (true ⇒? true) (true)
+:test (true ⇒? false) (false)
+:test (false ⇒? true) (true)
+:test (false ⇒? false) (true)
 
 # mathematical iff (if and only if) definition
-iff [[(1 =>? 0) && (0 =>? 1)]]
+iff [[(1 ⇒? 0) ⋀? (0 ⇒? 1)]]
 
-…<=>?… iff
+…⇔?… iff
 
-:test (true <=>? true) (true)
-:test (true <=>? false) (false)
-:test (false <=>? true) (false)
-:test (false <=>? false) (true)
+:test (true ⇔? true) (true)
+:test (true ⇔? false) (false)
+:test (false ⇔? true) (false)
+:test (false ⇔? false) (true)
diff --git a/std/Math.bruijn b/std/Math.bruijn
index db97d3c..ea2bf71 100644
--- a/std/Math.bruijn
+++ b/std/Math.bruijn
@@ -15,7 +15,7 @@ gcd z [[[(1 =? 0) case-eq ((1 >? 0) case-gre case-les)]]]
 :test ((gcd (+3) (+8)) =? ((+1))) (true)
 
 # power function
-pow [(!!) (iterate ((*) 0) (+1))]
+pow […!!… (iterate (…*… 0) (+1))]
 
 …**… pow
 
diff --git a/std/Number.bruijn b/std/Number.bruijn
index 60920aa..812a5c4 100644
--- a/std/Number.bruijn
+++ b/std/Number.bruijn
@@ -1,6 +1,6 @@
 # MIT License, Copyright (c) 2022 Marvin Borner
-# This file specifies the most basic mathematical operations
-# -> refer to std/Math for more advanced functions
+# This file defines the most basic mathematical operations
+# → refer to std/Math for more advanced functions
 # Heavily inspired by the works of T.Æ. Mogensen (see refs in README)
 
 :import std/Combinator .
@@ -8,73 +8,67 @@
 :import std/Logic .
 
 # negative trit indicating coeffecient of (-1)
-t< [[[2]]]
+t⁻ [[[2]]]
 
 # returns true if a trit is negative
-t<? [0 true false false]
+t⁻? [0 true false false]
 
 # positive trit indicating coeffecient of (+1)
-t> [[[1]]]
+t⁺ [[[1]]]
 
 # returns true if a trit is positive
-t>? [0 false true false]
+t⁺? [0 false true false]
 
 # zero trit indicating coeffecient of 0
-t= [[[0]]]
+t⁰ [[[0]]]
 
 # returns true if a trit is zero
-t=? [0 false false true]
-
-:test (t<? t<) (true)
-:test (t<? t>) (false)
-:test (t<? t=) (false)
-:test (t>? t<) (false)
-:test (t>? t>) (true)
-:test (t>? t=) (false)
-:test (t=? t<) (false)
-:test (t=? t>) (false)
-:test (t=? t=) (true)
+t⁰? [0 false false true]
+
+:test (t⁻? t⁻) (true)
+:test (t⁻? t⁺) (false)
+:test (t⁻? t⁰) (false)
+:test (t⁺? t⁻) (false)
+:test (t⁺? t⁺) (true)
+:test (t⁺? t⁰) (false)
+:test (t⁰? t⁻) (false)
+:test (t⁰? t⁺) (false)
+:test (t⁰? t⁰) (true)
 
 # shifts a negative trit into a balanced ternary number
-up-neg [[[[[2 (4 3 2 1 0)]]]]]
+↑⁻‣ [[[[[2 (4 3 2 1 0)]]]]]
 
-^<‣ up-neg
-
-:test (^<(+0)) ((-1))
-:test (^<(-1)) ((-4))
-:test (^<(+42)) ((+125))
+:test (↑⁻(+0)) ((-1))
+:test (↑⁻(-1)) ((-4))
+:test (↑⁻(+42)) ((+125))
 
 # shifts a positive trit into a balanced ternary number
-up-pos [[[[[1 (4 3 2 1 0)]]]]]
-
-^>‣ up-pos
+↑⁺‣ [[[[[1 (4 3 2 1 0)]]]]]
 
-:test (^>(+0)) ((+1))
-:test (^>(-1)) ((-2))
-:test (^>(+42)) ((+127))
+:test (↑⁺(+0)) ((+1))
+:test (↑⁺(-1)) ((-2))
+:test (↑⁺(+42)) ((+127))
 
 # shifts a zero trit into a balanced ternary number
-up-zero [[[[[0 (4 3 2 1 0)]]]]]
-
-^=‣ up-zero
+↑⁰‣ [[[[[0 (4 3 2 1 0)]]]]]
 
-:test (^=(+0)) ([[[[0 3]]]])
-:test (^=(+1)) ((+3))
-:test (^=(+42)) ((+126))
+:test (↑⁰(+0)) ([[[[0 3]]]])
+:test (↑⁰(+1)) ((+3))
+:test (↑⁰(+42)) ((+126))
 
 # shifts a specified trit into a balanced ternary number
 up [[[[[[5 2 1 0 (4 3 2 1 0)]]]]]]
 
-:test (up t< (+42)) (^<(+42))
-:test (up t> (+42)) (^>(+42))
-:test (up t= (+42)) (^=(+42))
+:test (up t⁻ (+42)) (↑⁻(+42))
+:test (up t⁺ (+42)) (↑⁺(+42))
+:test (up t⁰ (+42)) (↑⁰(+42))
 
 # shifts the least significant trit out - basically div by 3
-down [snd (0 z a< a> a=)]
+down [~(0 z a⁻ a⁺ a⁰)]
 	z (+0) : (+0)
-	a< [0 [[^<1 : 1]]]
-	a> [0 [[^>1 : 1]]]
-	a= [0 [[^=1 : 1]]]
+	a⁻ [0 [[↑⁻1 : 1]]]
+	a⁺ [0 [[↑⁺1 : 1]]]
+	a⁰ [0 [[↑⁰1 : 1]]]
 
 # negates a balanced ternary number
 negate [[[[[4 3 1 2 0]]]]]
@@ -86,20 +80,20 @@ negate [[[[[4 3 1 2 0]]]]]
 :test (-(+42)) ((-42))
 
 # converts a balanced ternary number to a list of trits
-list! [0 z a< a> a=]
+list! [0 z a⁻ a⁺ a⁰]
 	z [[0]]
-	a< [t< : 0]
-	a> [t> : 0]
-	a= [t= : 0]
+	a⁻ [t⁻ : 0]
+	a⁺ [t⁺ : 0]
+	a⁰ [t⁰ : 0]
 
 # TODO: Tests!
 
 # strips leading 0s from balanced ternary number
-strip [fst (0 z a< a> a=)]
+strip [^(0 z a⁻ a⁺ a⁰)]
 	z (+0) : true
-	a< [0 [[^<1 : false]]]
-	a> [0 [[^>1 : false]]]
-	a= [0 [[(0 (+0) ^=1) : 0]]]
+	a⁻ [0 [[↑⁻1 : false]]]
+	a⁺ [0 [[↑⁺1 : false]]]
+	a⁰ [0 [[(0 (+0) ↑⁰1) : 0]]]
 
 %‣ strip
 
@@ -108,27 +102,27 @@ strip [fst (0 z a< a> a=)]
 :test (%(+42)) ((+42))
 
 # extracts least significant trit from balanced ternary numbers
-lst [0 t= [t<] [t>] [t=]]
+lst [0 t⁰ [t⁻] [t⁺] [t⁰]]
 
-:test (lst (-1)) (t<)
-:test (lst (+0)) (t=)
-:test (lst (+1)) (t>)
-:test (lst (+42)) (t=)
+:test (lst (-1)) (t⁻)
+:test (lst (+0)) (t⁰)
+:test (lst (+1)) (t⁺)
+:test (lst (+42)) (t⁰)
 
 # extracts most significant trit from balanced ternary numbers
 # TODO: Find a more elegant way to do this (and resolve list import loop?)
 mst [fix (last (list! %0))]
-	last z [[<>?0 [false] [<>?(snd 1) (fst 1) (2 (snd 1))] i]]
+	last z [[<>?0 [false] [<>?(~1) ^1 (2 ~1)] i]]
 		<>?‣ [0 [[[false]]] true]
-	fix [((t<? 0) || ((t>? 0) || (t=? 0))) 0 t=]
+	fix [((t⁻? 0) ⋁? ((t⁺? 0) ⋁? (t⁰? 0))) 0 t⁰]
 
-:test (mst (-1)) (t<)
-:test (mst (+0)) (t=)
-:test (mst (+1)) (t>)
-:test (mst (+42)) (t>)
+:test (mst (-1)) (t⁻)
+:test (mst (+0)) (t⁰)
+:test (mst (+1)) (t⁺)
+:test (mst (+42)) (t⁺)
 
 # returns true if balanced ternary number is negative
-negative? [t<? (mst 0)]
+negative? [t⁻? (mst 0)]
 
 <?‣ negative?
 
@@ -138,7 +132,7 @@ negative? [t<? (mst 0)]
 :test (<?(+42)) (false)
 
 # returns true if balanced ternary number is positive
-positive? [t>? (mst 0)]
+positive? [t⁺? (mst 0)]
 
 >?‣ positive?
 
@@ -158,39 +152,39 @@ zero? [0 true [false] [false] i]
 :test (=?(+42)) (false)
 
 # converts the normal balanced ternary representation into abstract
-# -> the abstract representation is used in eq?/add/sub/mul
-abstract! [0 z a< a> a=]
+# → the abstract representation is used in eq?/add/sub/mul
+abstract! [0 z a⁻ a⁺ a⁰]
 	z (+0)
-	a< [[[[[2 4]]]]]
-	a> [[[[[1 4]]]]]
-	a= [[[[[0 4]]]]]
+	a⁻ [[[[[2 4]]]]]
+	a⁺ [[[[[1 4]]]]]
+	a⁰ [[[[[0 4]]]]]
 
-->^‣ abstract!
+→^‣ abstract!
 
-:test (->^(-3)) ([[[[0 [[[[2 [[[[3]]]]]]]]]]]])
-:test (->^(+0)) ([[[[3]]]])
-:test (->^(+3)) ([[[[0 [[[[1 [[[[3]]]]]]]]]]]])
+:test (→^(-3)) ([[[[0 [[[[2 [[[[3]]]]]]]]]]]])
+:test (→^(+0)) ([[[[3]]]])
+:test (→^(+3)) ([[[[0 [[[[1 [[[[3]]]]]]]]]]]])
 
 # converts the abstracted balanced ternary representation back to normal
 # using ω to solve recursion
 normal! ω rec
-	rec [[0 (+0) [^<([3 3 0] 0)] [^>([3 3 0] 0)] [^=([3 3 0] 0)]]]
+	rec [[0 (+0) [↑⁻([3 3 0] 0)] [↑⁺([3 3 0] 0)] [↑⁰([3 3 0] 0)]]]
 
-->_‣ normal!
+→_‣ normal!
 
-:test (->_[[[[3]]]]) ((+0))
-:test (->_(->^(+42))) ((+42))
-:test (->_(->^(-42))) ((-42))
+:test (→_[[[[3]]]]) ((+0))
+:test (→_(→^(+42))) ((+42))
+:test (→_(→^(-42))) ((-42))
 
 # checks whether two balanced ternary numbers are equal
 # larger numbers should be second argument (performance)
-# -> ignores leading 0s!
-eq? [[abs 1 ->^0]]
-	abs [0 z a< a> a=]
-		z [=?(->_0)]
-		a< [[0 false [2 0] [false] [false]]]
-		a> [[0 false [false] [2 0] [false]]]
-		a= [[0 (1 0) [false] [false] [2 0]]]
+# → ignores leading 0s!
+eq? [[abs 1 →^0]]
+	abs [0 z a⁻ a⁺ a⁰]
+		z [=?(→_0)]
+		a⁻ [[0 false [2 0] [false] [false]]]
+		a⁺ [[0 false [false] [2 0] [false]]]
+		a⁰ [[0 (1 0) [false] [false] [2 0]]]
 
 …=?… eq?
 
@@ -213,11 +207,11 @@ eq? [[abs 1 ->^0]]
 # the same. Something's weird.
 
 # adds (+1) to a balanced ternary number (can introduce leading 0s)
-inc [snd (0 z a< a> a=)]
+inc [~(0 z a⁻ a⁺ a⁰)]
 	z (+0) : (+1)
-	a< [0 [[^<1 : ^=1]]]
-	a> [0 [[^>1 : ^<0]]]
-	a= [0 [[^=1 : ^>1]]]
+	a⁻ [0 [[↑⁻1 : ↑⁰1]]]
+	a⁺ [0 [[↑⁺1 : ↑⁻0]]]
+	a⁰ [0 [[↑⁰1 : ↑⁺1]]]
 
 ++‣ inc
 
@@ -231,11 +225,11 @@ ssinc strip . inc
 :test ((++(+42)) =? (+43)) (true)
 
 # subs (+1) from a balanced ternary number (can introduce leading 0s)
-dec [snd (0 z a< a> a=)]
+dec [~(0 z a⁻ a⁺ a⁰)]
 	z (+0) : (-1)
-	a< [0 [[^<1 : ^>0]]]
-	a> [0 [[^>1 : ^=1]]]
-	a= [0 [[^=1 : ^<1]]]
+	a⁻ [0 [[↑⁻1 : ↑⁺0]]]
+	a⁺ [0 [[↑⁺1 : ↑⁰1]]]
+	a⁰ [0 [[↑⁰1 : ↑⁻1]]]
 
 --‣ dec
 
@@ -250,18 +244,18 @@ sdec strip . dec
 
 # adds two balanced ternary numbers (can introduce leading 0s)
 # larger numbers should be second argument (performance)
-add [[abs 1 ->^0]]
-	abs [c (0 z a< a> a=)]
-		b< [1 ^>(3 0 t<) ^=(3 0 t=) ^<(3 0 t=)]
-		b= [up 1 (3 0 t=)]
-		b> [1 ^=(3 0 t=) ^<(3 0 t>) ^>(3 0 t=)]
-		a< [[[1 (b< 1) b<' b= b<]]]
-			b<' [1 ^=(3 0 t<) ^<(3 0 t=) ^>(3 0 t<)]
-		a> [[[1 (b> 1) b= b>' b>]]]
-			b>' [1 ^>(3 0 t=) ^=(3 0 t>) ^<(3 0 t>)]
-		a= [[[1 (b= 1) b< b> b=]]]
-		z [[0 --(->_1) ++(->_1) ->_1]]
-		c [[1 0 t=]]
+add [[abs 1 →^0]]
+	abs [c (0 z a⁻ a⁺ a⁰)]
+		b⁻ [1 ↑⁺(3 0 t⁻) ↑⁰(3 0 t⁰) ↑⁻(3 0 t⁰)]
+		b⁰ [up 1 (3 0 t⁰)]
+		b⁺ [1 ↑⁰(3 0 t⁰) ↑⁻(3 0 t⁺) ↑⁺(3 0 t⁰)]
+		a⁻ [[[1 (b⁻ 1) b⁻' b⁰ b⁻]]]
+			b⁻' [1 ↑⁰(3 0 t⁻) ↑⁻(3 0 t⁰) ↑⁺(3 0 t⁻)]
+		a⁺ [[[1 (b⁺ 1) b⁰ b⁺' b⁺]]]
+			b⁺' [1 ↑⁺(3 0 t⁰) ↑⁰(3 0 t⁺) ↑⁻(3 0 t⁺)]
+		a⁰ [[[1 (b⁰ 1) b⁻ b⁺ b⁰]]]
+		z [[0 --(→_1) ++(→_1) →_1]]
+		c [[1 0 t⁰]]
 
 …+… add
 
@@ -313,35 +307,35 @@ les? \gre?
 
 # returns true if number is less than or equal to other number
 # smaller numbers should be second argument (performance)
-leq? [[!(1 >? 0)]]
+leq? [[¬(1 >? 0)]]
 
-…<=?… leq?
+…≤?… leq?
 
-:test ((+1) <=? (+2)) (true)
-:test ((+2) <=? (+2)) (true)
-:test ((+3) <=? (+2)) (false)
+:test ((+1) ≤? (+2)) (true)
+:test ((+2) ≤? (+2)) (true)
+:test ((+3) ≤? (+2)) (false)
 
 # returns true if number is greater than or equal to other number
 # smaller numbers should be second argument (performance)
 geq? \leq?
 
-…>=?… geq?
+…≥?… geq?
 
-:test ((+1) >=? (+2)) (false)
-:test ((+2) >=? (+2)) (true)
-:test ((+3) >=? (+2)) (true)
+:test ((+1) ≥? (+2)) (false)
+:test ((+2) ≥? (+2)) (true)
+:test ((+3) ≥? (+2)) (true)
 
 # returns max number of two
-max [[(1 <=? 0) 0 1]]
+max [[(1 ≤? 0) 0 1]]
 
 # returns min number of two
-min [[(1 <=? 0) 1 0]]
+min [[(1 ≤? 0) 1 0]]
 
 # muls two balanced ternary numbers (can introduce leading 0s)
-mul [[1 (+0) a< a> a=]]
-	a< [^=0 - 1]
-	a> [^=0 + 1]
-	a= [^=0]
+mul [[1 (+0) a⁻ a⁺ a⁰]]
+	a⁻ [↑⁰0 - 1]
+	a⁺ [↑⁰0 + 1]
+	a⁰ [↑⁰0]
 
 …*… mul