Change syntax language

docs/source/language/3.Hello,-world!.md

@@ -4,7 +4,7 @@
 
 This is the "Hello, World!" in Formality:
 
-```bash
+```haskell
 import Base@0
 
 main : Output
@@ -15,7 +15,7 @@ Save this as `hello.fm` and run it with `fm hello/main`. This will use the inter
 
 Formality is a pure functional language: it has no global state or built-in IO. Instead, it just evaluates expressions, stringifies and outputs the result. As such, `Output : Type` and `print : {str : String} -> Output` are really just base-library (included on the first line) utilities that tell the CLI to pretty-print a string. `main` doesn't need to be an `Output`, though. It can be anything. For example, run this instead:
 
-```bash
+```haskell
 import Base@0
 
 main : String
@@ -24,7 +24,7 @@ main : String
 
 And it will output:
 
-```bash
+```haskell
 {cons, nil} => cons(1819043144,
 {cons, nil} => cons(1998597231,
 {cons, nil} => cons(1684828783,
@@ -37,7 +37,7 @@ Which is how the string is encoded internally (a "Scott List" of 32-bit words st
 
 Formality is also a proof language, which means it includes a powerful type-checker. You can call it with `fm -t <file>/<term>`. If your program is well-typed, you'll see its type. Otherwise, you'll see an error message explaining what is wrong. For example, given the program below:
 
-```bash
+```haskell
 import Base@0
 
 main : String
@@ -56,7 +56,7 @@ Type mismatch.
 
 Because `42` isn't a `String`. It is recommended to **always check a program's type before running it**. Ill-typed programs aren't guaranteed to run correctly. Formality won't stop you from trying, though. In fact, type annotations are optional:
 
-```javascript
+```haskell
 import Base@0
 
 main

docs/source/language/4.Core-Features.md

@@ -4,15 +4,15 @@
 
 Formality includes `let` expressions, which allow you to give local names to terms.
 
-```javascript
+```haskell
 main : Output
   let hello = "Hello, world!"
   print(hello)
 ```
 
 `let` expressions can be infinitely nested.
 
-```javascript
+```haskell
 main : Output
   let output = 
     let hello = "Hello, world!"
@@ -26,7 +26,7 @@ Note that `let` has no computational effect. It simply performs a parse-time sub
 
 Formality includes native, unsigned, 32-bit numbers, and many numeric operations:
 
-name | syntax | JavaScript equivalent
+name | syntax | haskell equivalent
 --- | --- | ---
 addition | `x + y` | `(x + y) >>> 0`
 subtraction | `x - y` | `(x - y) >>> 0`
@@ -54,28 +54,28 @@ float-to-uint | `.u(y)` | -
 
 The type of a native number is `Word`. A number literal can be written in decimal:
 
-```javascript
+```haskell
 main : Word
   1900
 ```
 
 Or in hexadecimal:
 
-```javascript
+```haskell
 main : Word
   0x76C
 ```
 
 Or in binary:
 
-```javascript
+```haskell
 main : Word
   0b11101101100
 ```
 
 Operators work as expected, except there is no precedence: parenthesis are always placed on the right. An expression like `3 * 10 + 1`, for example, is always parsed as `3 * (10 + 1)`. If you want the multiplication to occur first, you must be explicit:
 
-```javascript
+```haskell
 main : Word
   (3 * 10) + 1
 ```
@@ -90,7 +90,7 @@ syntax | description
 
 Usage is straightforward:
 
-```javascript
+```haskell
 main : Output
   let age = 30
 
@@ -116,22 +116,22 @@ Note that the type of a pair is `[x : A, B(x)]`, because the type of the second
 
 Creating:
 
-```javascript
+```haskell
 main : [:Word, Word]
   [1, 2]
 ```
 
 Extracting the first element:
 
-```javascript
+```haskell
 main : Word
   let pair = [1, 2]
   fst(pair)
 ```
 
 Extracting both elements:
 
-```javascript
+```haskell
 main : Word
   let pair  = [1, 2]
   get [a,b] = pair
@@ -140,7 +140,7 @@ main : Word
 
 Nesting:
 
-```javascript
+```haskell
 main : [:[:Word, Word], String]
   [[1, 2], "Hello Word!"]
 ```
@@ -168,7 +168,7 @@ Formality functions are anonymous expressions, like Haskell's lambdas. There are
 
 A top-level function:
 
-```javascript
+```haskell
 adder : Word -> Word -> Word
   {x, y} x + y
 
@@ -178,7 +178,7 @@ main : Word
 
 When you write the variable names, lambdas are added implicity. For example:
 
-```javascript
+```haskell
 adder : {x : Word, y : Word} -> Word
   x + y
 
@@ -188,28 +188,28 @@ main : Word
 
 An inline function (lambda expression):
 
-```javascript
+```haskell
 main : Word
   ({x : Word, y : Word} x + y)(40, 2)
 ```
 
 You can annotate the full type rather than the type of each variable:
 
-```javascript
+```haskell
 main : Word
   (({x, y} x + y) :: Word -> Word -> Word)(40, 2)
 ```
 
 You can avoid types. This won't type-check, but can still be ran:
 
-```javascript
+```haskell
 main
   ({x, y} x + y)(40, 2)
 ```
 
 Lambdas and applications can be erased with a `~`, which causes them to vanish from the compiled output. This is useful, for example, to write polymorphic functions without extra runtime costs. For example, on the code below, `id` is compiled to `{x} x`, and `main` is compiled to `id(42)`. The first argument disappears from the runtime.
 
-```javascript
+```haskell
 id : {~T : Type, x : T} -> T
   x
 
@@ -220,7 +220,7 @@ main : Word
 
 Formality functions are **affine**, which means you can't use a variable more than once. For example, the program below isn't allowed, because `b` is used twice:
 
-```javascript
+```haskell
 copy : {b : Bool} -> [:Bool, Bool]
   [b, b]
 ```
@@ -274,7 +274,7 @@ syntax | description
 
 This is useful when the bidirectional type-checker can't infer the type of an expression.
 
-```javascript
+```haskell
 main : Word
   (({x, y} x + y) :: Word -> Word -> Word)(40, 2)
 ```
@@ -283,7 +283,7 @@ main : Word
 
 Formality also features holes, which are very useful for development and debugging. A hole can be used to fill a part of your program that you don't want to implement yet. It can be written anywhere as `?name`, with the name being optional. This will cause Formality to print the type expected on the hole location, as well as the its context (scope variables). For example, the program below:
 
-```javascript
+```haskell
 import Base@0
 
 main : {x : Bool} -> Bool
@@ -292,7 +292,7 @@ main : {x : Bool} -> Bool
 
 Will output:
 
-```javascript
+```
 [ERROR]
 Hole found.
 - With goal... Bool
@@ -307,9 +307,9 @@ The point of holes is that Formality will assume them to be true, allowing you t
 
 ## Logs
 
-Another handy feature is `log(x)`. When running a program, it will print the normal form of `x`, similarly to JavaScript's `console.log` and Python's `print`, but for anything (not only strings). When type-checking a program, it tells you the normal-form and the type of `x`. This is useful when you want to know what type an expression would have inside certain context. For example:
+Another handy feature is `log(x)`. When running a program, it will print the normal form of `x`, similarly to haskell's `console.log` and haskell's `print`, but for anything (not only strings). When type-checking a program, it tells you the normal-form and the type of `x`. This is useful when you want to know what type an expression would have inside certain context. For example:
 
-```javascript
+```haskell
 import Base@0
 
 main : {f : Bool -> Nat} -> Nat
@@ -334,7 +334,7 @@ Hole found.
 
 This tells you that, inside the body of `main`, the type of `f(true)` is `Nat`. Since it coincides with the type of the hole, you can complete the program above with it:
 
-```javascript
+```haskell
 import Base@0
 
 main : {f : Bool -> Nat} -> Nat
@@ -345,7 +345,7 @@ main : {f : Bool -> Nat} -> Nat
 
 The `import` statement can be used to include local files. For example, save an `Answers.fm` file in the same directory as `hello.fm`, with the following contents:
 
-```javascript
+```haskell
 import Base@0
 
 everything : String
@@ -354,7 +354,7 @@ everything : String
 
 Then save a `test.fm` file as:
 
-```javascript
+```haskell
 import Base@0
 import Answers
 
@@ -367,7 +367,7 @@ And run it with `fm test/main`. You should see `42`.
 If multiple imports have conflicting names, you can disambiguate with `File/name`, or with a qualified import, using `as`:
 
 
-```javascript
+```haskell
 import Base@0
 import Answers as A
 
@@ -379,7 +379,7 @@ main : Output
 
 Formality also has a file-based package manager. You can use it to share files with other people. A file can be saved globally with `fm -s file`. This will give it a unique name with a version, such as `file@7`. Once given a unique name, the file contents will never change, so `file@7` will always refer to that exact file. As soon as it is saved globally, you can import it from any other computer. For example, remove `Answers.fm` and change `hello.fm` to:
 
-```javascript
+```haskell
 import Base@0
 import Answers@0