.koder

NOTE ON CURRENT UPDATE

Kind has recently received many new syntaxes, which means many files are still
outdated. To update definitions, favor the equational notation. Also update
tests to use the '#test' notation. Example:

```
// Doubles a natural number.
// 1st: The number to double.
// = The double of the input number.
Nat/double
: ∀(n: Nat)
  Nat
= λ{
  #Zero: #Zero
  #Succ: λn.pred #Succ{#Succ{(Nat/double n.pred)}}
}
// Tests for the double function.

// Test: double 0 = 0
TEST_0
: (Equal Nat (Nat/double #Zero) #Zero)
= #Refl

// Test: double 1 = 2
TEST_1
: (Equal Nat (Nat/double #1) #2)
= #Refl
```

Must be updated to:

```
// Doubles a nat.
// - n: The nat to double.
// = The double of the input nat.
Nat/double : Nat -> Nat
| #Zero    = #Zero
| #Succ{n} = #Succ{#Succ{(Nat/double n)}}

#test: (Nat/double #0) == #0
#test: (Nat/double #1) == #2
```

We're also refactoring ADT declarations. Example:

```
// Propositional Equality.
// - A: The element type.
// - x: The 1st element.
// - y: The 2nd element.
// = A proposition that x equals y.
Equal : ∀(A: *) A -> A -> *
= λA λx λy
  data[y]{
    #Refl : (Equal A x x)
  } : (Equal A x y)
```

Must be updated to:

```
// Propositional Equality.
// - A: The element type.
// - x: The 1st element.
// - y: The 2nd element.
// = A proposition that x equals y.
data Equal (A: *) ~ (x: A) (y: A) {
  #Refl : (Equal A x x)
}
```

NOTE: ADT indices must be placed after '~' on its signature

NOTE: the return type of an ADT Ctr (ex: '#Refl : (Equal A x x)') can be omitted when the ADT isn't indexed

NOTE: tests should always be one-liners, and without comments.

NOTE: keep comments concise and less redundant. Example:

Instead of:

"The type of elements in the input list."

You should write:

"Input type."

In general, current comments are overly verbose and you should make them more terse and objective.

NOTE: auxiliary functions should be called "/go" (not "/aux" nor "/helper"), and should be placed AFTER the main function, note before.

NOTE: you should use 'if x { t } else { f }' (where 'x' is a Bool, not an U32) instead of U32/if or similar

NOTE: U32 functions like '==' and '>' return an U32, not a Bool. when a Bool is needed, use U32/to-bool

NOTE: do not create tests with functions that you've not been explicitly shown. you tend to hallucinate functions that don't exist. don't do that.

NOTE: do NOT change the logic or algorithm used in the implementations in any way. just update to the newer syntax, keeping the same logic closely.

NOTE: always use the same field names when pattern-matching equations. do not use '_'. example:

NOTE: '#3' makes a Nat (sugar for #Succ{#Succ{#Succ{#Zero}}}) and '3' makes an U32 (native)

| #Cons{_  _}  #Nil         = A
| #Cons{a0 as} #Cons{b0 bs} = B

this isn't allowed, because 'a0' and '_' have different names, despite corresponding to the same field. write this instead:

| #Cons{a0 as} #Nil         = A
| #Cons{a0 as} #Cons{b0 bs} = B

NOTE: never use Type/match functions. just use a match expression ('match x { ... }')