Improved wiki and reduced readme

3 files changed, 109 insertions, 26 deletions

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
+```