Improved wiki and reduced readme

22 files changed, 532 insertions, 76 deletions

diff --git a/docs/wiki_src/coding/IO.md b/docs/wiki_src/coding/IO.md
index 974f98e..c1abc8a 100644
--- a/docs/wiki_src/coding/IO.md
+++ b/docs/wiki_src/coding/IO.md
@@ -11,6 +11,12 @@ You can use [`std/Monad`](/std/Monad.bruijn.html) to interact with the
 input monadically, or simply use [`std/List`](/std/List.bruijn.html)
 operations to work with the input as a normal list.
 
+See [data structures](data-structures.md) to learn more about lists and
+numbers.
+
+If you want your main function to ignore the input, just add an
+additional (unbound) abstraction to your definition.
+
 ## Example
 
 ``` bruijn
diff --git a/docs/wiki_src/coding/REPL.md b/docs/wiki_src/coding/REPL.md
index a801ef9..e3ec1a7 100644
--- a/docs/wiki_src/coding/REPL.md
+++ b/docs/wiki_src/coding/REPL.md
@@ -1,6 +1,6 @@
 # REPL
 
-The REPL is a very helpful feature for functional programming languages
+The REPL is a very helpful tool for functional programming languages
 like bruijn. You can use it to continuously test or execute parts of
 your code.
 
@@ -8,6 +8,8 @@ You can start the REPL using `stack run`{.bash} or (if installed)
 `bruijn`{.bash}.
 
 Any valid term will get reduced to normal form after pressing enter.
+Common [data structures](data-structures.md) will get resolved in a
+seperate line if detected (e.g. numbers, lists or strings).
 
 ## Definitions
 
@@ -82,9 +84,9 @@ unreduced and the reduced expression. Helpful for golfed
 [compilation](compilation.md).
 
 ``` bruijn
-> :blc [0] [0]
-0100100010
-0010
+> :length [0] [0]
+10
+4
 ```
 
 ### `:free`{.bruijn}
diff --git a/docs/wiki_src/coding/combinators.md b/docs/wiki_src/coding/combinators.md
index e69de29..b85b7fa 100644
--- a/docs/wiki_src/coding/combinators.md
+++ b/docs/wiki_src/coding/combinators.md
@@ -0,0 +1,74 @@
+# Combinators
+
+Combinators are short *closed* terms that can be combined with other
+terms or combinators.
+
+## Common
+
+All of these combinators (and many more) can be found in
+[`std/Combinator`](/std/Combinator.bruijn.html). The names are taken
+from Raymond Smullyan's book "To Mock a Mockingbird"[^1].
+
+`y`{.bruijn}/`z`{.bruijn}: *Fixed-point* combinators
+
+:   used to achieve [recursion](recursion.md)
+
+:   `(y g)`{.bruijn} = `(g (y g))`{.bruijn}
+
+`b`{.bruijn}/`b'`{.bruijn}/`b'''`{.bruijn} or `…∘…`{.bruijn}/`…∘∘…`{.bruijn}/`…∘∘∘…`{.bruijn}: *Blackbird* combinators
+
+:   used to compose two functions with 1/2/3 arguments
+
+:   `((f ∘ g) x)`{.bruijn} = `(f (g x))`{.bruijn}
+
+:   `(((f ∘∘ g) x) y)`{.bruijn} = `(f ((g x) y))`{.bruijn}
+
+:   `((((f ∘∘∘ g) x) y) z)`{.bruijn} = `(f (((g x) y) z))`{.bruijn}
+
+`c`{.bruijn} or `\‣`{.bruijn}: *Cardinal* combinator
+
+:   used to flip arguments (e.g. for higher-order application)
+
+:   `((\f x) y)`{.bruijn} = `((f y) x)`{.bruijn}
+
+`s`{.bruijn} or `…<*>…`{.bruijn}: *Starling* combinator
+
+:   used to apply one argument to two functions (*substitution*)
+
+:   `((f <*> g) x)`{.bruijn} = `((f x) (g x))`{.bruijn}
+
+`k`{.bruijn} or `const`{.bruijn}: *Kestrel* combinator
+
+:   used to wrap a term inside an additional abstraction (also for
+    [boolean logic](data-structures.md#booleansbits-stdlogic))
+
+:   `(k f)`{.bruijn} = `[f]`{.bruijn}
+
+`i`{.bruijn} (Haskell's `id`{.haskell}): *Kestrel* combinator
+
+:   used as identity function or to indicate an unused argument
+
+:   `(i x)`{.bruijn} = `x`{.bruijn}
+
+`ψ`{.bruijn}: *Psi* combinator (Haskell's `on`{.haskell})
+
+:   used to apply two arguments to one function seperately
+
+:   `((((ψ f) g) x) y)`{.bruijn} = `((f (g x)) (g y))`{.bruijn}
+
+`ω`{.bruijn}: *Mockingbird*/*omega* combinator
+
+:   used to apply a term to itself
+
+:   `(ω f)`{.bruijn} = `(f f)`{.bruijn}
+
+:   Also: `Ω`{.bruijn} = `(ω ω)`{.bruijn}
+
+------------------------------------------------------------------------
+
+If you enjoy the use of combinators, you might also enjoy bruijn's
+sister language [Birb](https://esolangs.org/wiki/Birb).
+
+[^1]: Smullyan, Raymond M. To Mock a Mockingbird: and other logic
+    puzzles including an amazing adventure in combinatory logic. Oxford
+    University Press, USA, 2000.
diff --git a/docs/wiki_src/coding/currying.md b/docs/wiki_src/coding/currying.md
index d84eb0a..9a8e48d 100644
--- a/docs/wiki_src/coding/currying.md
+++ b/docs/wiki_src/coding/currying.md
@@ -1,13 +1,29 @@
 # Currying
 
-Lambda calculus naturally supports currying -- that is, only partially
+Lambda calculus naturally supports currying -- that is, only *partially*
 applying a function. In fact *any* function can be applied with *any*
 amount of arguments!
 
 In bruijn, currying is a great way to make functions even more elegant.
 
-Partially applying the `mul`{.bruijn} function:
+For example, take the negation function:
 
 ``` bruijn
-six [0 (+3)] (mul (+2))
+# subtracts argument from zero
+-‣ [(+0) - 0] ⧗ Number → Number
+
+# equivalent curried version
+-‣ sub (+0)
+```
+
+Currying is also very useful for higher-order functions.
+
+Multiplying values in a list by partially applying the `mul`{.bruijn}
+function:
+
+``` bruijn
+# doubles numbers in a list
+double-list [0 <$> (mul (+2))] ⧗ (List Number) → (List Number)
+
+:test (double-list ((+1) : {}(+2))) ((+2) : {}(+4))
 ```
diff --git a/docs/wiki_src/coding/data-structures.md b/docs/wiki_src/coding/data-structures.md
index 384ac29..0516bf7 100644
--- a/docs/wiki_src/coding/data-structures.md
+++ b/docs/wiki_src/coding/data-structures.md
@@ -62,7 +62,8 @@ a-box <>'a'
 
 ## Pairs [`std/Pair`](/std/Pair.bruijn.html)
 
-Pairs (tuples) can store any two terms.
+Pairs (tuples) can store any two terms. Pairs can be constructed using
+the `…:…`{.bruijn} [mixfix](mixfix.md) function.
 
 Example:
 
@@ -82,6 +83,11 @@ Lists are a repeated composition (right-associative) of pairs with a
 (heterogeneous) values and are recursively iterable. The call-by-need
 reduction order of bruijn allows lazy evaluation (i.e. infinite lists).
 
+Due to the right-associativeness, writing lists by hand is slightly
+annoying. The usage of the `…:…`{.bruijn} [mixfix](mixfix.md) and
+`{}‣`{.bruijn} [prefix](prefix.md) functions to denote pairs and the
+final `empty`{.bruijn} symbol is encouraged.
+
 Example:
 
 ``` bruijn
@@ -90,10 +96,19 @@ Example:
 :test ((foldr …+… (+0) ((+1) : ((+2) : {}(+3)))) =? (+6)) (true)
 ```
 
+The internal structure of the list encoding means that when a list is
+applied to a function, the function is called with the head and tail of
+the list.
+
+``` bruijn
+:test ("abc" [[1]]) ('a')
+:test ("abc" [[0]]) ("bc")
+```
+
 ## Strings [`std/String`](/std/String.bruijn.html)
 
 Strings are just a list of binary encoded bytes. You may use
-[`std/List`](/std/List.bruijn.html) in combinatoin with
+[`std/List`](/std/List.bruijn.html) in combination with
 [`std/Number/Binary`](/std/Binary.bruijn.html) to interact with them.
 
 Example:
diff --git a/docs/wiki_src/coding/examples.md b/docs/wiki_src/coding/examples.md
index e69de29..f4d0b62 100644
--- a/docs/wiki_src/coding/examples.md
+++ b/docs/wiki_src/coding/examples.md
@@ -0,0 +1,134 @@
+# Examples
+
+## Hello world!
+
+Hello world using [lists](../coding/data-structures.md#lists-stdlist)
+and [IO](../coding/IO.md)!
+
+``` bruijn
+:import std/List .
+
+main ["Hello " ++ 0 ++ "!\n"]
+```
+
+``` bash
+$ printf "world" | bruijn file.bruijn
+Hello world!
+```
+
+## Syntax
+
+Example functions demonstrating the syntax without usage of
+[`std/`](/std/).
+
+``` bruijn
+# this is a comment
+# returns ternary 1 (syntactic sugar)
+get-one (+1)
+
+# we can use the function in all functions below its definition
+get-one2 get-one
+
+# tests are similar to assertions in other languages
+# they test equality using α-equivalence of reduced expressions
+:test (get-one2) ((+1))
+
+# indenting acts similarly to Haskell's where statement
+get-one3 foo
+    bar (+1)
+    foo bar
+
+# equivalent of λx.x or Haskell's id x = x
+id [0]
+
+# testing equivalent of (λx.x) (λx.λy.x) = λx.λy.x
+# the numbers in the abstractions refer to arguments using
+# De Bruijn indices
+:test (id [[1]]) ([[1]])
+
+# prefix function definition
+!‣ [[1]]
+
+# use prefix function '!'
+# ![0] becomes ([[1]] [0]) which in turn becomes [[0]]
+:test (![0]) ([[0]])
+
+# infix function definition: flip and apply arguments
+…<>… [[0 1]]
+
+# use infix function '<>'
+# [[0]] <> [[1]] becomes (([[0 1]] [[0]]) [[1]])
+:test ([[0]] <> [[1]]) ([[1]] [[0]])
+
+# multiple arguments
+number-set set-of-three (+1) (+2) (+3)
+    set-of-three [[[[0 1 2 3]]]]
+
+access-first [0 [[[0]]]]
+
+:test (access-first number-set) ((+1))
+
+# ignore stdin and return string
+main ["Hello world!\n"]
+```
+
+## Standard library
+
+``` bruijn
+:import std/Combinator .
+:import std/List .
+:import std/Logic .
+:import std/Number .
+:import std/Option .
+:import std/Pair .
+
+# pairs with some values
+love pair me you
+    me [[[1]]]
+    you [[[2]]]
+
+:test (fst love) ([[[1]]])
+:test (snd love) ([[[2]]])
+
+# you can also write (me : you) instead of (pair me you)
+# also ^love and ~love instead of (fst love) and (snd love)
+
+# numerical operations
+# remember that every mixfix chain is left-associative
+five --((+8) + (-4) - (-2))
+
+not-five? [if (0 =? (+5)) false true]
+
+# awesome mixfix functions
+:test (∑ (+1) → (+3) | [++0]) ((+9))
+:test (∏ (+1) → (+3) | [++0]) ((+24))
+
+:test (not-five? five) (false)
+
+:test ((uncurry mul (pair (+3) (+2))) =? (+6)) (true)
+
+# lazy evaluation using infinite lists and indexing
+pow2 …!!… (iterate (…⋅… (+2)) (+1))
+
+:test ((pow2 (+5)) =? (+32)) (true)
+
+# options
+:test (map inc (some (+1))) (some (+2))
+:test (apply (some (+1)) [some ++0]) (some (+2))
+
+# boolean
+# the main function gets executed automatically
+# ignore stdin arguments by not referencing 0
+main [¬(false ⋀? true ⋁? true)]
+
+:test (main [0]) (false)
+```
+
+## More examples
+
+You can find more example programs in
+[`samples/`](https://github.com/marvinborner/bruijn/tree/main/samples)
+of our source-code repository. The samples include several solutions to
+[Advent of Code](https://adventofcode.com/) problems.
+
+Reading the source of the [standard library](/std/) can also be helpful.
diff --git a/docs/wiki_src/coding/laziness.md b/docs/wiki_src/coding/laziness.md
index feec480..20d1205 100644
--- a/docs/wiki_src/coding/laziness.md
+++ b/docs/wiki_src/coding/laziness.md
@@ -45,8 +45,8 @@ example:
 :time ((+10) ** (+500)) =? (+400)
 ```
 
-This works because a ternary number is just a list of trits which (in
-this case) gets recursively generated by the `pow`{.bruijn} function.
-The `eq?`{.bruijn} function just throws away the first argument if it's
-already clear that the numbers can't be equal (in this case after the
-first argument got bigger than `(+400)`{.bruijn}).
+This works because a ternary number is just a concatenation of trits
+which (in this case) gets recursively generated by the `pow`{.bruijn}
+function. The `eq?`{.bruijn} function just throws away the first
+argument if it's already clear that the numbers can't be equal (in this
+case after the first argument got bigger than `(+400)`{.bruijn}).
diff --git a/docs/wiki_src/coding/mixfix.md b/docs/wiki_src/coding/mixfix.md
index c85b936..f42d0ab 100644
--- a/docs/wiki_src/coding/mixfix.md
+++ b/docs/wiki_src/coding/mixfix.md
@@ -1,9 +1,9 @@
 # Mixfix
 
 Mixfix functions allow arbitrary infix operations based on "substitution
-holes" by using the `…` symbol in (special character) definitions. The
-symbols and terms always need to be delimited by a space character, else
-they get interpreted as a [prefix](prefix.md).
+holes" by using the `…` symbol in definitions. The symbols and terms
+always need to be delimited by a space character, otherwise they get
+interpreted as a [prefix](prefix.md).
 
 Example:
 
@@ -31,3 +31,24 @@ literally:
 ``` bruijn
 :test (…+… (+4) (+3)) (add (+4) (+3))
 ```
+
+## Associativity
+
+If you write several mixfix operations without parenthesis, they will be
+reduced in left-associative order. Just make sure that the longer mixfix
+chain is not actually overwritten by *another* mixfix chain.
+
+``` bruijn
+:test ((+8) + (-4) ⋅ (-2)) ((-8))
+
+# (don't do this)
+…+…⋅… [[[(+16)]]]
+
+:test ((+8) + (-4) ⋅ (-2)) ((+16))
+```
+
+## Allowed characters
+
+Mixfix functions can use any characters of `!?*@:;+-_#$%^&<>/\|{}~=` as
+well as mathematical unicode operators and arrows. Each part must be at
+least 1 character long.
diff --git a/docs/wiki_src/coding/performance.md b/docs/wiki_src/coding/performance.md
deleted file mode 100644
index e69de29..0000000
--- a/docs/wiki_src/coding/performance.md
+++ /dev/null
diff --git a/docs/wiki_src/coding/prefix.md b/docs/wiki_src/coding/prefix.md
index 589e081..64f36e9 100644
--- a/docs/wiki_src/coding/prefix.md
+++ b/docs/wiki_src/coding/prefix.md
@@ -11,7 +11,7 @@ Example:
 
 ``` bruijn
 # defines a negation prefix function called '-'
--‣ [(+0) - 0]
+-‣ [(+0) - 0] ⧗ Number → Number
 
 # returns 0 - 10 = -10
 :test (-(+10)) ((-10))
@@ -23,3 +23,9 @@ literally:
 ``` bruijn
 :test (-‣ (+10)) ((-10))
 ```
+
+## Allowed characters
+
+Prefix functions can use any characters of `!?*@:;+-_#$%^&<>/\|{}~=` as
+well as mathematical unicode operators and arrows. They must be at least
+1 character long.
diff --git a/docs/wiki_src/coding/recursion.md b/docs/wiki_src/coding/recursion.md
index 68148e5..9625ef9 100644
--- a/docs/wiki_src/coding/recursion.md
+++ b/docs/wiki_src/coding/recursion.md
@@ -28,7 +28,7 @@ outer argument is the initial function again.
 Example for using `y`{.bruijn} to find the factorial of 2:
 
 ``` bruijn
-# here, `1` is the outer argument (y g)
+# here, `1` is the induced outer argument `(y g)`
 # `0` is the accumulator (the argument of `factorial`)
 g [[=?0 (+1) (0 ⋅ (1 --0))]]
 
@@ -37,7 +37,7 @@ factorial y g ⧗ Number → Number
 :test ((factorial (+3)) =? (+6)) (true)
 ```
 
-In-the-wild, this could look like this.
+In the wild it might look like this:
 
 ``` bruijn
 # 3 abstractions => two arguments
@@ -50,7 +50,9 @@ length z [[[rec]]] (+0) ⧗ (List a) → Number
         case-end 1
 ```
 
-Also see [coding style](style.md) for other style suggestions.
+Read [list data structure](data-structures.md#lists-stdlist) for more
+information. Also read [coding style](style.md) for other style
+suggestions.
 
 ## Mutual recurrence relations
 
@@ -69,9 +71,9 @@ g [[[=?0 true (1 --0)]]]
 # the even? recursive call will be the first argument (2)
 h [[[=?0 false (2 --0)]]]
 
-even? head (y* g h) ⧗ Number → Bool
+even? head (y* g h) ⧗ Number → Boolean
 
-odd? tail (y* g h) ⧗ Number → Bool
+odd? tail (y* g h) ⧗ Number → Boolean
 ```
 
 Read more about this in the blog post [Variadic fixed-point
diff --git a/docs/wiki_src/coding/style.md b/docs/wiki_src/coding/style.md
index d0ec7a9..a9621d7 100644
--- a/docs/wiki_src/coding/style.md
+++ b/docs/wiki_src/coding/style.md
@@ -1,16 +1,59 @@
 # Coding style
 
-## Scoping
+## Program
+
+-   Every function has to be delimited by one empty line.
+-   Every (non-scoped) function must have a comment directly above it.
+-   Tests must appear in a single block (no empty lines) one line under
+    the definition.
+
+See the [standard library](/std/) for inspiration.
+
+## Function naming
+
+De Bruijn indices can be seen as a disadvantage to readability. It's
+therefore much more important to name the functions appropriately.
+
+For functions that return a boolean, we suggest using the suffix `?`. If
+your function has different cases it's recommended to use the `case-`
+prefix in scoped sub-terms.
+
+``` bruijn
+# from std/Ternary
+zero? [0 case-end case-neg case-pos i] ⧗ Number → Boolean
+    case-end true
+    case-neg [false]
+    case-pos [false]
+```
+
+Appropriate [type signatures](../introduction/syntax.md#types) are also
+encouraged.
 
 ## If/else
 
-redundant
+Since booleans are just lambda terms either returning its first or
+second argument, the use of if/else procedures is generally redundant.
+See [bit/boolean data
+structure](data-structures.md#booleansbits-stdlogic).
+
+``` bruijn
+:test (true 'a' 'b') ('a')
+:test (false 'a' 'b') ('b')
+```
 
 ## Head/tail
 
-redundant
+The internal structure of the list encoding means that when a list is
+applied to a function, the function is called with the head and tail of
+the list.
+
+``` bruijn
+:test ("abc" [[1]]) ('a')
+:test ("abc" [[0]]) ("bc")
+```
 
-## Type signatures
+Therefore the recommended style for coding with lists is to use
+`head`{.bruijn}/`tail`{.bruijn} only when truly needed.
 
 ## Recursion
 
diff --git a/docs/wiki_src/coding/test-driven-development.md b/docs/wiki_src/coding/test-driven-development.md
index f62c448..56c1bf1 100644
--- a/docs/wiki_src/coding/test-driven-development.md
+++ b/docs/wiki_src/coding/test-driven-development.md
@@ -6,21 +6,22 @@ creating functions, we suggest the following procedure:
 -   Write a comment, a type signature, and the head of the function
 
 ``` bruijn
-# measures the length of a list
-length y [[[rec]]] (+0) ⧗ (List a) → Number
+# returns the item at index in a list, starting from 0
+index y [[[rec]]] ⧗ (List a) → Number → a
 ```
 
--   Write several tests including all edge cases
+-   Write several tests including edge cases
 
 ``` bruijn
-# measures the length of a list
-length y [[[rec]]] (+0) ⧗ (List a) → Number
-
-:test (length empty) ((+0))
-:test (length "a") ((+1))
-:test (length ({}empty)) ((+1))
-:test (length (empty : {}empty)) ((+2))
-:test (length ("abc")) ((+3))
+# returns the item at index in a list, starting from 0
+index y [[[rec]]] ⧗ (List a) → Number → a
+
+:test (empty !! (+0)) (empty)
+:test ({}(+1) !! (+0)) ((+1))
+:test (((+1) : ((+2) : {}(+3))) !! (+0)) ((+1))
+:test (((+1) : ((+2) : {}(+3))) !! (+2)) ((+3))
+:test (((+1) : ((+2) : {}(+3))) !! (-1)) (empty)
+:test (((+1) : ((+2) : {}(+3))) !! (+3)) (empty)
 ```
 
 -   Finish the implementation until all tests pass (e.g. using the
@@ -28,15 +29,16 @@ length y [[[rec]]] (+0) ⧗ (List a) → Number
 -   Refactor and clean up the definition
 
 ``` bruijn
-# measures the length of a list
-length y [[[rec]]] (+0) ⧗ (List a) → Number
-    rec 0 [[[case-inc]]] case-end
-        case-inc 5 ++4 1
-        case-end 1
-
-:test (length empty) ((+0))
-:test (length "a") ((+1))
-:test (length ({}empty)) ((+1))
-:test (length (empty : {}empty)) ((+2))
-:test (length ("abc")) ((+3))
+# returns the item at index in a list, starting from 0
+index y [[[rec]]] ⧗ (List a) → Number → a
+    rec 0 [[[case-index]]] case-end
+        case-index =?4 2 (5 --4 1)
+        case-end empty
+
+:test (empty !! (+0)) (empty)
+:test ({}(+1) !! (+0)) ((+1))
+:test (((+1) : ((+2) : {}(+3))) !! (+0)) ((+1))
+:test (((+1) : ((+2) : {}(+3))) !! (+2)) ((+3))
+:test (((+1) : ((+2) : {}(+3))) !! (-1)) (empty)
+:test (((+1) : ((+2) : {}(+3))) !! (+3)) (empty)
 ```
diff --git a/docs/wiki_src/coding/typing.md b/docs/wiki_src/coding/typing.md
deleted file mode 100644
index e69de29..0000000
--- a/docs/wiki_src/coding/typing.md
+++ /dev/null
diff --git a/docs/wiki_src/coding/uniform-function-call-syntax.md b/docs/wiki_src/coding/uniform-function-call-syntax.md
index e69de29..3999961 100644
--- a/docs/wiki_src/coding/uniform-function-call-syntax.md
+++ b/docs/wiki_src/coding/uniform-function-call-syntax.md
@@ -0,0 +1,14 @@
+# Uniform function call syntax (UFCS)
+
+UFCS is a syntactic feature that allows you to use functions in a
+different (perhaps more "natural") order.
+
+By using the dot `.` between two terms, the first term will be applied
+to the second term instead of the other way around.
+
+Example:
+
+``` bruijn
+:test ("abc".length) (length "abc")
+:test ("abc".length.inc) ((+4))
+```
diff --git a/docs/wiki_src/index.md b/docs/wiki_src/index.md
index 3049322..000f874 100644
--- a/docs/wiki_src/index.md
+++ b/docs/wiki_src/index.md
@@ -3,4 +3,6 @@
 Bruijn is basically pure lambda calculus with a bit of syntactic sugar.
 It has no side effects, primitive functions or datatypes.
 
-Browse this wiki by using the search or by clicking *next* or any of the links.
+Browse this wiki by using the search or by clicking *next* or any of the
+links. If you prefer free-flowing text, read the blog post [The bruijn
+programming language](https://text.marvinborner.de/2023-04-06-01.html).
diff --git a/docs/wiki_src/introduction/lambda-calculus.md b/docs/wiki_src/introduction/lambda-calculus.md
index 59a7c59..574c5ee 100644
--- a/docs/wiki_src/introduction/lambda-calculus.md
+++ b/docs/wiki_src/introduction/lambda-calculus.md
@@ -4,33 +4,38 @@ Bruijn is based on De Bruijn indexed lambda calculus.
 
 ## Traditional lambda calculus
 
-Lambda calculus basically has three types of expressions:
+Lambda calculus basically has three types of terms:
 
--   *Variable*: `x` represents another expression.
--   *Abstraction*: `λx.E` accepts an argument x and binds it to
-    expression `E` respectively. It's helpful to think of abstractions
-    as anonymous functions.
+-   *Variable*: `x` binds the named variable `x` to an abstraction.
+-   *Abstraction*: `λx.E` accepts an argument `x` and binds it to term
+    `E` respectively. It's helpful to think of abstractions as anonymous
+    functions.
 -   *Application*: `(f x)` applies `f` to `x` -- the standard convention
     allows repeated left-associative application: `(f x y z)` is
     `(((f x) y) z)`.
 
-Combining these expressions and removing redundant parentheses can
-result in expressions like λx.λy.x y, basically representing a function
-with two parameters that uses its second parameter as an argument for
-its first.
+Combining these terms and removing redundant parentheses can result in
+terms like λx.λy.x y, basically representing a function with two
+parameters that uses its second parameter as an argument for its first.
 
-Evaluating expressions is called *reduction*. There's only one rule you
-need to know: `((λx.E) A)` becomes `E[x := A]` -- that is, calling an
-abstraction with an argument substitutes the argument inside the
-expression of the abstraction ("β-reduction"). There are many different
-kinds of reduction techniques, but they basically all come back to this
-simple rule -- mainly because of the "Church-Rosser theorem" that states
-that the order of reduction doesn't change the eventual result.
+Evaluating terms is called *reduction*. There's only one rule you need
+to know: `((λx.E) A)` becomes `E[x := A]` -- that is, calling an
+abstraction with an argument substitutes the argument inside the body of
+the abstraction ("β-reduction"). There are many different kinds of
+reduction techniques, but they basically all come back to this simple
+rule -- mainly because of the "Church-Rosser theorem" that states that
+the order of reduction doesn't change the eventual result.
 
 When we talk about reduction in bruijn, we typically mean "reduction
 until normal form" -- we reduce until the term can't be reduced any
 further (there does not exist any `((λx.E) A)`).
 
+``` bruijn
+((λx.x) (λx.x))    ⤳ (λx.x)
+((λx.x) (λx.λy.x)) ⤳ (λx.λy.x)
+((λx.λy.x) (λx.x)) ⤳ (λy.λx.x)
+```
+
 ## De Bruijn indices
 
 Programs written in lambda calculus often have many abstractions and
diff --git a/docs/wiki_src/introduction/setup.md b/docs/wiki_src/introduction/setup.md
index 92f9886..e47ea6f 100644
--- a/docs/wiki_src/introduction/setup.md
+++ b/docs/wiki_src/introduction/setup.md
@@ -1,6 +1,52 @@
 # Setup
 
--   unicode keymap
--   editors
--   syntax highlighting
--   broogle
+In theory you can use any common editor and operating system. Please
+create an [issue on
+GitHub](https://github.com/marvinborner/bruijn/issues/new) if you have
+problems setting up bruijn.
+
+## Recommended setup
+
+The recommended setup is to use [Vim](https://www.vim.org/) and its
+bruijn plugin.
+
+The Vim plugin adds syntax highlighting for bruijn files as well as a
+custom keymap for typing commonly used unicode symbols.
+
+### Installation
+
+1.  Use Vim and [vim-plug](https://github.com/junegunn/vim-plug) (or
+    comparable plugin managers)
+2.  Add `"Plug 'marvinborner/bruijn', { 'rtp': 'editors/vim' }"` to your
+    `.vimrc`
+3.  Run `:PlugInstall`
+
+### Unicode abbreviations
+
+You can find all abbreviations in
+[`editors/vim/syntax/bruijn.vim`](https://github.com/marvinborner/bruijn/blob/main/editors/vim/syntax/bruijn.vim).
+Abbreviations get replaced after pressing space or `C-]`. Feel free to
+suggest improvements or create your own abbreviations.
+
+## Alternatives
+
+We have a Kate XML syntax highlighting file in
+[`editors/kate/bruijn.xml`](https://github.com/marvinborner/bruijn/blob/main/editors/kate/bruijn.xml),
+although it has *not* actually been tested with Kate (only as a syntax
+highlighting file for `pandoc`).
+
+## Broogle
+
+Broogle is a tool for searching standard library functions by name, type
+signatures, or comment. It's highly inspired by Haskell's
+[hoogle](https://hoogle.haskell.org/).
+
+You can use it after cloning [bruijn's
+repository](https://github.com/marvinborner/bruijn) and installing `rg`
+(`ripgrep`), `jq`, `sed`, and `awk`.
+
+``` bash
+./broogle.sh -t "a -> a"
+./broogle.sh -f "i"
+./broogle.sh -c "idiot combinator"
+```
diff --git a/docs/wiki_src/introduction/syntax.md b/docs/wiki_src/introduction/syntax.md
index 55e2c21..4dbc784 100644
--- a/docs/wiki_src/introduction/syntax.md
+++ b/docs/wiki_src/introduction/syntax.md
@@ -5,12 +5,16 @@ an esoteric programming language. Most notably the usage of lambda
 calculus logic, combinators, and De Bruijn indices can be confusing at
 first -- it's definitely possible to get used to them though!
 
-Bruijn uses a [variation of lambda calculus](lambda-calculus.md).
+Bruijn uses a [variation of lambda calculus](lambda-calculus.md). For
+subjective syntax rules, read [coding style](../coding/style.md). Also
+see the [examples](../coding/examples.md).
 
 ## Definitions
 
 Bruijn works by defining named substitution rules, where each usage of
-the identifier will get substituted respectively.
+the identifier will get substituted respectively. You can't use
+definitions before they are defined, every file gets substituted from
+top to bottom.
 
 Since there's no other major syntactic block, bruijn omits the equal
 symbol for definitions.
@@ -55,7 +59,7 @@ closed1 [[[2 0] 1]]
 
 Bruijn does not give warnings for open terms and reduces them as normal.
 In some cases it's actually encouraged to use open terms as sub-terms
-for better readability (see [coding style
+for improved readability (see [coding style
 suggestions](../coding/style.md)).
 
 ## Imports
@@ -101,8 +105,8 @@ After running:
           reduced to [[1]] = [[0]]
 
 Tests are always run for the executed file and any files it contains. If
-they take too long, you can enable the *YOLO* mode by using bruijn's
-`-y` argument.
+they take too long and you're sure your code is correct, you can enable
+the *YOLO* mode to disable tests by using bruijn's `-y` argument.
 
 ## Scoping
 
@@ -145,4 +149,32 @@ structures](../coding/data-structures.md).
 
 ## Types
 
-TODO.
+As of right now, typing is entirely optional and *purely* for
+documentation/aesthetics. Aside from syntax, types do not get checked in
+any way.
+
+We do have plans to implement type checking in the future, unfortunately
+almost all trivial typing mechanisms for pure lambda calculus reduce its
+power immensely.
+
+The current syntax of types is quite simple:
+
+    POLYMORPHIC := [a-z]+
+    CONSTRUCTOR := ([A-Z][a-z]* TYPE)
+    FUNCTION    := (TYPE → ... → TYPE)
+    IDENTIFIER  := [A-Z][a-z]*
+    TYPE        := IDENTIFIER | TYPE-VARIABLE | CONSTRUCTOR | FUNCTION
+    SIGNATURE   := TYPE → ... → Type
+
+The type signature can be written at the end of any bruijn term using
+the `⧗`{.bruijn} symbol.
+
+Examples:
+
+``` bruijn
+# from std/Combinator
+c [[[2 0 1]]] ⧗ (a → b → c) → b → a → c
+
+# from std/List
+empty? [0 [[[false]]] true] ⧗ (List a) → Boolean
+```
diff --git a/docs/wiki_src/technical/arithmetic.md b/docs/wiki_src/technical/arithmetic.md
deleted file mode 100644
index e69de29..0000000
--- a/docs/wiki_src/technical/arithmetic.md
+++ /dev/null
diff --git a/docs/wiki_src/technical/performance.md b/docs/wiki_src/technical/performance.md
new file mode 100644
index 0000000..05fd683
--- /dev/null
+++ b/docs/wiki_src/technical/performance.md
@@ -0,0 +1,24 @@
+# Performance
+
+The reduction of lambda calculus is (practically) not very efficient. As
+an extension, bruijn also suffers from bad performance.
+
+Bruijn's interpreter works by substituting the entire program into one
+huge lambda calculus term that will then get reduced by the
+[reducer](reduction.md). As a result, many equivalent terms get
+evaluated multiple times (although some of this get's solved by bruijn's
+call-by-need reduction strategy). We currently work on a solution that
+reduces all equivalent terms as one, which turns out is not actually
+that trivial. Follow the [blog](https://text.marvinborner.de) to keep up
+to date with the development.
+
+Aside from that, bruijn is still much faster than most of the hobby
+programming languages based on pure lambda calculus. This is because of
+the [RKNL reducer](reduction.md) and our choice of default [number/byte
+encodings](../coding/data-structures.md).
+
+``` bruijn
+> :import std/Math .
+> :time fac (+30)
+0.15 seconds
+```
diff --git a/docs/wiki_src/technical/reduction.md b/docs/wiki_src/technical/reduction.md
index e69de29..97bd78f 100644
--- a/docs/wiki_src/technical/reduction.md
+++ b/docs/wiki_src/technical/reduction.md
@@ -0,0 +1,12 @@
+# Reduction
+
+Bruijn uses the RKNL abstract machine reducer[^1]. RKNL uses the
+call-by-need reduction strategy, similar to Haskell and other functional
+programming languages. For you this means that you have efficient
+support for [laziness](../coding/laziness.md) with generally less
+redundant reductions.
+
+[^1]: [Biernacka, Małgorzata, Witold Charatonik, and Tomasz Drab. "A
+    simple and efficient implementation of strong call by need by an
+    abstract machine." Proceedings of the ACM on Programming Languages
+    6.ICFP (2022): 109-136.](https://doi.org/10.5281/zenodo.6786796)