Minor orthographic improvements

docs/index.html

@@ -5,7 +5,7 @@
     <meta name="viewport" content="width=device-width" />
     <meta
       name="description"
-      content="Functional programming language based on pure De Bruijn indexed lambda calculus."
+      content="Functional programming language based on pure de Bruijn indexed lambda calculus."
     />
     <link rel="stylesheet" href="style.css" type="text/css" media="all" />
     <title>bruijn programming language</title>
@@ -28,7 +28,7 @@ <h1>bruijn</h1>
 
       <div class="right">
         <p>
-          Functional programming language based on pure De Bruijn indexed lambda
+          Functional programming language based on pure de Bruijn indexed lambda
           calculus.
         </p>
       </div>

docs/script.js

@@ -29,12 +29,12 @@ const describe = (c, d) => {
 	[...document.getElementsByClassName(c)].forEach(el => el.addEventListener("click", e => notify(d, e)));
 }
 
-describe("binary", "Syntactic sugar for a binary number representation using abstractions as data. Needs a sign and brackets to differentiate it from De Bruijn indices");
+describe("binary", "Syntactic sugar for a binary number representation using abstractions as data. Needs a sign and brackets to differentiate it from de Bruijn indices");
 describe("char", "Syntactic sugar for a binary representation of characters using abstractions as data.");
 describe("com", "This indicates a command to the interpreter. The most common commands are :test (verifying α-equivalency) and :import (importing definitions from other files).");
 describe("def", "This defines a new term substitution. Using this identifier will substitute the term on its right side.");
 describe("header", "[0] is the identity operation. It returns the first argument it gets. Nothing more.");
-describe("index", "This number references the nth abstraction, starting counting from the inside. These 'De Bruijn indices' replace the concept of variables in lambda calculus.");
+describe("index", "This number references the nth abstraction, starting counting from the inside. These 'de Bruijn indices' replace the concept of variables in lambda calculus.");
 describe("left-abs", "The opening bracket of a function abstraction. It's basically the equivalent of the λ in lambda calculus.");
 describe("left-app", "The opening bracket of a function application.");
 describe("meta", "This is the quote operator. It converts any given expression to bruijn's meta encoding. The meta encoding can be used for self modification and can be turned back to normal bruijn code.");
@@ -46,8 +46,8 @@ describe("right-app", "The closing bracket of a function application.");
 describe("stack", "Stack is a dependency manager for Haskell. Install it using the corresponding instructions for your operating system.")
 describe("string", "Syntactic sugar for a list of binary encoded chars.")
 describe("symbol", "This substitutes a previously defined term (for example from the standard library).");
-describe("ternary", "Syntactic sugar for a balanced ternary number representation using abstractions as data. Needs a sign and brackets to differentiate it from De Bruijn indices.");
+describe("ternary", "Syntactic sugar for a balanced ternary number representation using abstractions as data. Needs a sign and brackets to differentiate it from de Bruijn indices.");
 describe("time", "Incredibly fast for lambda calculus standards.");
-describe("unary", "Syntactic sugar for a unary number representation using abstractions as data. This is commonly known as a Church numeral. Needs a sign and brackets to differentiate it from De Bruijn indices.");
+describe("unary", "Syntactic sugar for a unary number representation using abstractions as data. This is commonly known as a Church numeral. Needs a sign and brackets to differentiate it from de Bruijn indices.");
 
 document.body.addEventListener("click", clearPopups, true)

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))

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.
 

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.
 

readme.md

@@ -3,7 +3,7 @@
 </p>
 
 > A purely functional programming language based on lambda calculus and
-> De Bruijn indices written in Haskell.
+> de Bruijn indices written in Haskell.
 
 Pronunciation: `/bɹaʊn/`.
 

src/Helper.hs

@@ -407,7 +407,7 @@ decimalToUnary n | n < 0     = decimalToUnary 0
   gen 0  = Bruijn 0
   gen n' = Application (Bruijn 1) (gen (n' - 1))
 
--- Decimal to De Bruijn encoding
+-- Decimal to de Bruijn encoding
 decimalToDeBruijn :: Integer -> Expression
 decimalToDeBruijn n | n < 0     = decimalToDeBruijn 0
                     | otherwise = gen n

std/Number/Bruijn.bruijn

@@ -1,18 +1,18 @@
 # MIT License, Copyright (c) 2023 Marvin Borner
-# De Bruijn numeral system (named by me)
+# de Bruijn numeral system (named by me)
 # proof that this numeral system does not support zero/eq/sub/etc. is in
 #   Wadsworth, Christopher. "Some unusual λ-calculus numeral systems."
 # very sad indeed
 
-# increments De Bruijn numeral
+# increments de Bruijn numeral
 inc [[[2 1]]]
 
 ++‣ inc
 
 :test (++(+0d)) ((+1d))
 :test (++(+5d)) ((+6d))
 
-# decrements De Bruijn numeral
+# decrements de Bruijn numeral
 dec [[1 0 0]]
 
 --‣ dec