Minor orthographic improvements

3 files changed, 20 insertions, 20 deletions

diff --git a/docs/wiki_src/coding/meta-programming.md b/docs/wiki_src/coding/meta-programming.md
index a77ecbe..c3577ca 100644
--- a/docs/wiki_src/coding/meta-programming.md
+++ b/docs/wiki_src/coding/meta-programming.md
@@ -37,7 +37,7 @@ again.
 :test (`[0 `,[0]]) (`[0 [0]])
 ```
 
-Unquoted De Bruijn indices will get bound to the respective abstraction
+Unquoted de Bruijn indices will get bound to the respective abstraction
 outside of its meta encoding.
 
 ``` bruijn
@@ -46,7 +46,7 @@ add-two `[0 + (+2u)]
 
 :test (!add-two (+2u)) ((+4u))
 
-# adds two using a reaching De Bruijn index
+# adds two using a reaching de Bruijn index
 add-two* [`(,0 + (+2u))]
 
 :test (!(add-two* `(+2u))) ((+4u))
diff --git a/docs/wiki_src/introduction/lambda-calculus.md b/docs/wiki_src/introduction/lambda-calculus.md
index 067eaad..0d6af8e 100644
--- a/docs/wiki_src/introduction/lambda-calculus.md
+++ b/docs/wiki_src/introduction/lambda-calculus.md
@@ -1,6 +1,6 @@
 # Lambda calculus
 
-Bruijn is based on De Bruijn indexed lambda calculus.
+Bruijn is based on de Bruijn indexed lambda calculus.
 
 ## Traditional lambda calculus
 
@@ -11,15 +11,15 @@ Lambda calculus basically has three types of terms:
     `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
+    allows repeated left-associative application: `f x y z` is
     `(((f x) y) z)`.
 
 Combining these terms and removing redundant parentheses can result in
-terms like λx.λy.x y, basically representing a function with two
+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 terms is called *reduction*. There's only one rule you need
-to know: `((λx.E) A)` becomes `E[x := A]` -- that is, calling an
+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
@@ -28,11 +28,11 @@ 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)`).
+further (there does not exist any `(λx.E A)`).
 
-    ((λx.x) (λx.x))    ⤳ (λx.x)
-    ((λx.x) (λx.λy.x)) ⤳ (λx.λy.x)
-    ((λx.λy.x) (λx.x)) ⤳ (λy.λx.x)
+    (λ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
 
@@ -43,15 +43,15 @@ many variables it's also really complicated to compare two expressions,
 since you first need to resolve shadowed and conflicting variables
 ("α-conversion").
 
-De Bruijn replace the concept of variables by using numeric references
-to the abstraction layer. Let me explain using an example: The
-expression `λx.x` becomes `λ0` -- the `0` refers to the first parameter
-of the abstraction. Subsequently, the expression `λx.λy.x y` becomes
-`λλ1 0`. Basically, if you're reading from left to right starting at the
-abstraction you want to bind, you increment on every occurring `λ` until
-you arrive at the index.
+De Bruijn indices replace the concept of variables by using numeric
+references to the abstraction layer. Let me explain using an example:
+The expression `λx.x` becomes `λ0` -- the `0` refers to the first
+parameter of the abstraction. Subsequently, the expression `λx.λy.x y`
+becomes `λλ1 0`. Basically, if you're reading from left to right
+starting at the abstraction you want to bind, you increment on every
+occurring `λ` until you arrive at the index.
 
-While confusing at first, programs written with De Bruijn indices can
+While confusing at first, programs written with de Bruijn indices can
 actually be way easier to understand than the equivalent program with
 named variables.
 
diff --git a/docs/wiki_src/introduction/syntax.md b/docs/wiki_src/introduction/syntax.md
index e14f8c6..7a3256d 100644
--- a/docs/wiki_src/introduction/syntax.md
+++ b/docs/wiki_src/introduction/syntax.md
@@ -2,7 +2,7 @@
 
 Bruijn has an arguably weird syntax, although it's not strictly meant as
 an esoteric programming language. Most notably the usage of lambda
-calculus logic, combinators, and De Bruijn indices can be confusing at
+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). For
@@ -42,7 +42,7 @@ normal lambda calculus reducer.
 
 ## Open terms
 
-If you use De Bruijn indices that reach out of their environment, you
+If you use de Bruijn indices that reach out of their environment, you
 have created an *open term*. Depending on the context, these terms are
 typically seen as invalid if standing by themself.