### Running Acorn Prover Website Locally (npm)

Source: https://github.com/acornprover/acornprover.org/blob/master/README.md

This command sequence installs necessary Node.js dependencies and then starts the local development server for the Acorn theorem prover website. It allows users to preview changes before deployment.

```Shell
npm install
npm start
```

--------------------------------

### Implicit Currying Example (Acorn)

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/functions.md

This example demonstrates Acorn's implicit currying. A two-argument function `add_then_double` is defined, and then partially applied with the argument `3` to create a new single-argument function `add_three_then_double`, illustrating how functions can be partially applied.

```acorn
define add_then_double(a: Nat, b: Nat) -> Nat {
    2 * (a + b)
}

let add_three_then_double: Nat -> Nat = add_then_double(3)
```

--------------------------------

### Citing Proven Theorems in Proofs (Acorn)

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/functions.md

This example demonstrates how a previously proven theorem, `add_zero_left`, can be explicitly cited and used as a step or hint within a subsequent proof. This allows for modularity in proofs, leveraging established theorems to simplify new derivations.

```acorn
theorem zero_plus_seven {
    0 + 7 = 7
} by {
    add_zero_left(7)
}
```

--------------------------------

### Example Proof by Contradiction in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/if-else.md

This example provides a concrete proof by contradiction for the theorem `2 * a != 2 * b + 3`. It assumes the negation (`2 * a = 2 * b + 3`) within the `if` block and derives `false`, thereby proving the original theorem.

```acorn
theorem foo(a: Nat, b: Nat) {
  2 * a != 2 * b + 3
} by {
  if 2 * a = 2 * b + 3 {
    2 * a  = 2 * (b + 1) + 1
    2 * (a - (b + 1)) = 1
    false
  }
}
```

--------------------------------

### Example Acorn Prover Build Cache Entry

Source: https://github.com/acornprover/acornprover.org/blob/master/blog/2025-03-13-the-build-cache.md

This snippet illustrates a human-readable entry from the Acorn Prover's build cache. It shows the recorded dependencies for the `add_from_int` theorem, indicating its reliance on specific theorems from the `rat` and `real` modules, which represent the premise selection work performed by the prover.

```Configuration
  add_from_int:
    rat:
    - add_int_eq_int_add
    real:
    - Real.from_int
    - add_from_rat
```

--------------------------------

### Acorn Single-Line Comment Syntax

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/indirect-proofs.md

This snippet demonstrates the syntax for single-line comments in Acorn, starting with `//`. Comments are used to provide human-readable explanations within the code without affecting its execution.

```Acorn
// By the division theorem
```

--------------------------------

### Demonstrating Compile-time Errors in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/multi-step-proofs.md

This snippet provides an example of code that will produce a red squiggle, indicating a compile-time error in Acorn. It uses undefined identifiers ('blorf', 'blonk', 'flump') to show how the prover flags syntax or semantic issues before proof checking.

```acorn
theorem {
    blorf + blonk = flump
}
```

--------------------------------

### Demonstrating Rat Operators in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/rat.md

This example showcases the use of arithmetic and comparison operators with `Rat` numbers after declaring `Rat` as a numeral type. It illustrates addition, multiplication, subtraction, division (with division by zero resulting in zero), negation, and various comparison operations.

```Acorn
numerals Rat

// Typical addition, multiplication, subtraction.
2 * (1 + 3) = 9 - 1

// Division by zero is defined to be zero, because Acorn functions must be defined on their whole domain.
1 / 0 = 0

// Negation.
-3 = -(6 / 2)

// Comparison.
1/2 < 1
2 <= 3
5 > 4
7 >= 0
```

--------------------------------

### Defining a Simple Named Function (Acorn)

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/functions.md

This example demonstrates the definition of a simple named function `square` in Acorn. It takes a natural number `n` as input and returns its square, showcasing the basic usage of the `define` keyword for function creation.

```acorn
define square(n: Nat) -> Nat {
    n * n
}
```

--------------------------------

### Defining `predecessor` Function by Satisfaction (Acorn)

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/functions.md

This example defines the `predecessor` function using the `let ... satisfy` construct. It specifies that the return value `p` should be `0` if the input `n` is `0`, otherwise `p.suc` (successor of `p`) should equal `n`, demonstrating conditional definition by satisfaction.

```acorn
let predecessor(n: Nat) -> p: Nat satisfy {
    if n = 0 {
        p = 0
    } else {
        p.suc = n
    }
}
```

--------------------------------

### Proving threeven_everywhere with Separate Base and Inductive Step Theorems in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/induction.md

This example demonstrates an inductive proof strategy where the base case and the inductive step are defined as separate theorems. The `base_case` theorem proves `threeven_nearby(0)`, while the `inductive_step` theorem proves that `threeven_nearby(n)` implies `threeven_nearby(n + 1)`, using a proof by cases. Acorn implicitly uses these to prove `threeven_everywhere(n)`.

```Acorn
define threeven_nearby(n: Nat) -> Bool {
    threeven(n) or threeven(n + 1) or threeven(n + 2)
}

theorem base_case {
    threeven_nearby(0)
}

theorem inductive_step(n: Nat) {
    threeven_nearby(n) implies threeven_nearby(n + 1)
} by {
    if threeven(n) {
        threeven(n + 3)
        threeven_nearby(n + 1)
    } else {
        threeven(n + 1) or threeven(n + 2)
        threeven_nearby(n + 1)
    }
}

theorem threeven_everywhere(n: Nat) {
    threeven_nearby(n)
}
```

--------------------------------

### Proving lt_cancel_suc Theorem in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/basic-concepts.md

This example from the standard library demonstrates a complete theorem with its proof steps. The theorem `lt_cancel_suc` proves that if `a.suc < b.suc`, then `a < b`. The `by` block contains individual statements (expressions) that serve as proof steps, leveraging premises and aiming to prove the conclusion.

```acorn
theorem lt_cancel_suc(a: Nat, b: Nat) {
    a.suc < b.suc implies a < b
} by {
    a.suc <= b.suc
    b.suc != a.suc
    a <= b and b != a
}
```

--------------------------------

### Creating a Structure Instance with new Method in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/structure-types.md

This example shows how to instantiate a 'LatticePoint' object using the implicitly generated 'new' method. The 'new' method acts as a constructor, taking arguments corresponding to the structure's fields.

```Acorn
let origin: LatticePoint = LatticePoint.new(0, 0)
```

--------------------------------

### Checking Integer Divisibility in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/int.md

This snippet demonstrates the `divides` predicate, which checks if one integer divides another. It includes examples with positive, negative, and zero values, showing cases where division holds true and where it does not.

```Acorn
divides(3, 9)
divides(2, -4)
divides(-5, 10)
divides(5, 0)
not divides(0, -1)
```

--------------------------------

### Illustrative Acorn Expressions

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/basic-concepts.md

This snippet provides various examples of expressions in Acorn, covering logical operations, arithmetic calculations, function calls, and equality checks. Expressions are fundamental building blocks that represent values or ways to construct them.

```acorn
// Logic
p implies q
p or q
p and q
not p
true
false

// Arithmetic
1 + 1
(1 + 2) * 3
2 + 2 < 5

// Calling functions
foo(bar, baz, qux)

// An equality is an expression
2 + 2 = 4

// Expressions can get complicated
exists(d: Nat) { d > 1 and d != n and exists(q: Nat) { q * d = n } }
```

--------------------------------

### Checking Linear Combination Spanning in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/int.md

This snippet demonstrates the `spans` function, which determines if an integer `c` can be expressed as a linear combination of two other integers `a` and `b`. It shows examples where `c` can and cannot be spanned.

```Acorn
spans(6, 10, 2)
not spans(6, 10, 3)
```

--------------------------------

### Quantifying Over a Single Variable in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/quantifiers.md

This example demonstrates the use of the `exists` quantifier to assert the existence of a natural number `b` that is greater than a given natural number `a`, proving the theorem 'there is always a bigger number'.

```acorn
theorem there_is_always_a_bigger_number(a: Nat) {
    exists(b: Nat) {
        b > a
    }
}
```

--------------------------------

### Executing Multiple GCD Steps - Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/nat_gcd.md

Demonstrates the result of applying the `gcd_step` function `n` times. This example shows `gcd_step` applied 10 times to the initial pair `(1000, 17)`, resulting in the final state `(1, 0)` where 1 is the GCD.

```acorn
gcd_step(NatPair.new(1000, 17), 10) = NatPair.new(1, 0)
```

--------------------------------

### Declaring Threeven Kinda Follows Throdd Theorem in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/indirect-proofs.md

This snippet declares the `threeven_kinda_follows_throdd` theorem, which states that if a number `n` is throdd, then either `n + 1` or `n + 2` must be threeven. This theorem serves as an example for proof by cases.

```Acorn
theorem threeven_kinda_follows_throdd(n: Nat) {
    throdd(n) implies threeven(n + 1) or threeven(n + 2)
}
```

--------------------------------

### Importing Specific Components from an Acorn Module

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/imports.md

This example illustrates importing specific names (`Nat`, `divides`) from the `nat` module directly into the current scope using `from ... import ...`. This allows `Nat` and `divides` to be used without the `nat.` prefix, making the code cleaner. However, this approach can lead to naming conflicts if multiple modules export the same name.

```Acorn
from nat import Nat, divides
numerals Nat

theorem even_nearby(n: Nat) {
  divides(2, n) or divides(2, n + 1)
} by {
  let (q: Nat, r: Nat) satisfy {
    r < 2 and n = q * 2 + r
  }
  if r = 0 {
    divides(2, n)
  } else {
    r = 1
    n = q * 2 + 1
    n + 1 = (q + 1) * 2
    divides(2, n + 1)
  }
}
```

--------------------------------

### Checking Divisibility in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/nat.md

This snippet demonstrates the `divides` predicate, which determines if one natural number divides another. A notable rule is that every number is considered to divide zero. The example shows `divides(5, 10)`.

```Acorn
divides(5, 10)
```

--------------------------------

### Checking if an Integer is Negative in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/int.md

This snippet demonstrates the `Int.is_negative` method, which returns `Bool` indicating whether an integer is negative. It shows examples where negative numbers return true, and positive numbers or zero return false.

```Acorn
i(-2).is_negative
not 2.is_negative
not 0.is_negative
```

--------------------------------

### Higher-Order Logic: Quantifying Over Functions in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/quantifiers.md

This example illustrates Acorn's support for higher-order logic by demonstrating quantification over functions. It uses `exists` to assert the existence of an injective function `f` from `Nat` to `Nat` such that for all natural numbers `a`, `f(a)` is greater than a given `n`.

```acorn
theorem bigifying_surjection(n: Nat) {
    exists(f: Nat -> Nat) {
        injective(f) and forall(a: Nat) {
            f(a) > n
        }
    }
}
```

--------------------------------

### Checking Decreasing to Zero Function - Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/nat_gcd.md

Illustrates the `decreasing_to_zero` function, which verifies if a natural number function strictly decreases until it reaches zero. The example uses a simple anonymous function `n - 1` to demonstrate this property.

```acorn
decreasing_to_zero(function(n: Nat) { n - 1 })
```

--------------------------------

### Proving Constraint Inhabitability for Structure Types in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/structure-types.md

This snippet illustrates how to explicitly prove that a constrained type is 'inhabited' (i.e., instances satisfying the constraint can exist) using a 'by' block. It provides a concrete example (first=0, second=1) that satisfies the 'first <= second' constraint for 'OrderedIntPair'.

```Acorn
structure OrderedIntPair {
    first: Int
    second: Int
} constraint {
    first <= second
} by {
    let first: Int = 0
    let second: Int = 1
    first <= second
}
```

--------------------------------

### Proving a Generic Theorem for a Typeclass in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/typeclasses.md

This example demonstrates how to declare a theorem that applies generically to any type `M` that is an instance of the `MetricSpace` typeclass. The `<M: MetricSpace>` syntax specifies this typeclass constraint, allowing the use of typeclass attributes like `x.distance` within the theorem's scope.

```acorn
theorem distance_non_negative<M: MetricSpace>(x: M, y: M) {
    not x.distance(y).is_negative
}
```

--------------------------------

### Calculating Factorial in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/nat.md

This snippet demonstrates the `factorial` function, which computes the factorial of a natural number. The factorial of a non-negative integer `n` is the product of all positive integers less than or equal to `n`. The example shows `factorial(3) = 6`.

```Acorn
factorial(3) = 6
```

--------------------------------

### Defining a Constrained Structure Type in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/structure-types.md

This example demonstrates how to define a 'constrained type' in Acorn by adding a 'constraint' block to a structure definition. The 'OrderedIntPair' structure requires that its 'first' field is less than or equal to its 'second' field.

```Acorn
structure OrderedIntPair {
    first: Int
    second: Int
} constraint {
    first <= second
}
```

--------------------------------

### Simple Variable Assignments in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/variables.md

These examples demonstrate basic variable assignments in Acorn. Variables `two` and `three` are assigned numeric values, and `two_less_than_three` is assigned a boolean result from a comparison. These assignments do not require proof as they are direct definitions of valid expressions.

```acorn
let two: Nat = 2

let three: Nat = 2.suc

let two_less_than_three: Bool = two < three
```

--------------------------------

### Calculating Greatest Common Divisor - Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/nat_gcd.md

Demonstrates the `gcd` function, which computes the greatest common divisor of two natural numbers using the Euclidean algorithm. The example shows `gcd(15, 10)` correctly resulting in `5`.

```acorn
gcd(15, 10) = 5
```

--------------------------------

### Defining Function Types in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/basic-concepts.md

This snippet illustrates how function types are defined in Acorn, specifying their argument and return types. Examples include functions taking one natural number and returning another (e.g., successor) and functions taking two natural numbers and returning one (e.g., addition).

```acorn
// Functions that take a natural number and return another.
// For example, "successor".
Nat -> Nat

// Functions that take two natural numbers and return another.
// For example, "addition".
(Nat, Nat) -> Nat
```

--------------------------------

### Checking False Below a Number - Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/nat_gcd.md

Shows how to use `false_below` to check if a given function `f` returns `false` for all natural numbers strictly less than `n`. An example `equals_one_hundred` is defined and then used to demonstrate `false_below` for numbers below 50.

```acorn
define equals_one_hundred(n: Nat) {
    n = 100
}

false_below(equals_one_hundred, 50)
```

--------------------------------

### Defining an `is_even` Predicate (Acorn)

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/functions.md

This example defines a logical predicate `is_even` that determines if a natural number `n` is even. It returns a `Bool` by checking for the existence of another natural number `d` such that `2 * d` equals `n`, illustrating predicate definition using existential quantification.

```acorn
define is_even(n: Nat) -> Bool {
    exists(d: Nat) {
        2 * d = n
    }
}
```

--------------------------------

### Mapping Class Attributes to Typeclass Attributes in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/typeclasses.md

This example shows how a type's own defined attribute (e.g., `Color.discrete`) can be used to fulfill a typeclass's attribute requirement (e.g., `MetricSpace.distance`). It highlights the explicit syntax required to differentiate between typeclass attributes and class attributes when accessed directly.

```acorn
class Color {
    define discrete(self, other: Color) -> Real {
        if x = y {
            0
        } else {
            1
        }
    }
}

instance Color: MetricSpace {
    let distance: (Color, Color) -> Real = Color.discrete
}
```

--------------------------------

### Assigning Max Value using If-else Expression in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/if-else.md

This example shows how to use an `if-else` expression to assign the maximum of two natural numbers, `a` and `b`, to a variable `max_a_b`. It highlights the use of `if-else` as an expression that returns a value.

```acorn
let max_a_b: Nat = if a < b {
    b
} else {
    a
}
```

--------------------------------

### Defining Multiple Variables Conditionally with `let satisfy` in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/variables.md

This example extends the `let ... satisfy` construct to define multiple variables, `d` and `n`, simultaneously based on a shared condition. Both variables are natural numbers that satisfy the equation `2 * d = n`, implying `n` is an even number and `d` is half of `n`. This also requires proof.

```acorn
let (d: Nat, n: Nat) satisfy {
    2 * d = n
}
```

--------------------------------

### Accessing Structure Fields with Object-Based Projection in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/structure-types.md

This example illustrates an alternative, more concise dot syntax for accessing structure fields directly on the object instance. 'origin.y' is equivalent to 'LatticePoint.y(origin)', providing a convenient way to retrieve field values.

```Acorn
theorem origin_y_is_zero {
    origin.y = 0
}
```

--------------------------------

### Encapsulating Code with `problem` Block in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/imports.md

This snippet demonstrates the use of a `problem` block in Acorn to define code that is verified internally but not exposed or visible outside the block. Variables (`a`, `b`) and theorems defined within this block are local to it and cannot be imported or referenced elsewhere in the file. This is useful for internal proofs, examples, or training AI models without affecting the external API of the module.

```Acorn
problem {
    let a: Nat = 2
    let b: Nat = 4
    theorem {
      a + a = b
    }
}
```

--------------------------------

### Deploying Acorn Prover Website to Production (npm)

Source: https://github.com/acornprover/acornprover.org/blob/master/README.md

This command initiates the deployment process for the Acorn theorem prover website to its production environment. It typically builds the site and pushes it to the configured hosting.

```Shell
npm run deploy
```

--------------------------------

### Defining Generic Pair Structure in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/blog/2025-02-26-generics.md

This snippet defines a generic `Pair` structure in Acorn, allowing it to encapsulate two values of arbitrary types `T` and `U`. It serves as a fundamental example of how to declare structures with multiple type parameters, enabling flexible data aggregation.

```acorn
structure Pair<T, U> {
    first: T
    second: U
}
```

--------------------------------

### Existential Quantifier for Logical Equivalence in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/variables.md

This snippet demonstrates using the `exists` quantifier to state a logical proposition without defining new variables in the outer scope. It asserts the existence of natural numbers `d` and `n` such that `2 * d = n`, which is logically equivalent to the previous `let satisfy` examples but keeps `d` and `n` scoped only within the `exists` block. This statement also requires proof.

```acorn
exists(d: Nat, n: Nat) {
    2 * d = n
}
```

--------------------------------

### Implicit Projection Theorem for Structure Fields in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/structure-types.md

This snippet shows another implicit theorem, 'projection', which guarantees that applying projection methods to a newly constructed structure will retrieve the original arguments used during its creation. For example, 'LatticePoint.new(x, y).x' will always equal 'x'.

```Acorn
theorem projection(x: Int, y: Int) {
    LatticePoint.new(x, y).x = x and LatticePoint.new(x, y).y = y
}
```

--------------------------------

### Defining Multi-step Proofs in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/multi-step-proofs.md

This snippet demonstrates the basic structure of a multi-step proof in Acorn using the 'by' keyword. It shows how a theorem statement can be followed by a proof block containing a sequence of logical steps, where each step is expected to be inferable from previous steps or premises.

```acorn
theorem cool_theorem {
    my_premise implies interesting_conclusion
} by {
    first_step
    second_step
    third_step
}
```

--------------------------------

### Demonstrating Int Operators in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/int.md

This snippet illustrates various arithmetic and comparison operators supported by the `Int` type in Acorn. It shows three ways to perform addition, multiplication, and subtraction (infix, static method, and instance method), two ways for negation, and three ways for each comparison operator (less than, less than or equal to, greater than, greater than or equal to).

```Acorn
numerals Int

// Three ways of adding two numbers.
2 + 2
Int.add(2, 2)
2.add(2)

// Three ways of multiplying two numbers.
2 * 2
Int.mul(2, 2)
2.mul(2)

// Three ways of subtracting two numbers.
4 - 2
Int.sub(4, 2)
4.sub(2)

// Two ways to negate a number.
-3
3.neg

// Three ways for each comparison operator.
2 < 3
Int.lt(2, 3)
2.lt(3)

2 <= 3
Int.lte(2, 3)
2.lte(3)

5 > 4
Int.gt(5, 4)
5.gt(4)

7 >= 0
Int.gte(7, 0)
7.gte(0)
```

--------------------------------

### Proving 'threeven_plus_three' with Multi-steps in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/multi-step-proofs.md

This snippet provides a multi-step proof for the 'threeven_plus_three' theorem. It uses the 'let ... satisfy' construct to introduce a variable 'd' based on the premise 'threeven(n)', and then shows the algebraic step '3 * (d + 1) = n + 3' to complete the proof.

```acorn
theorem threeven_plus_three(n: Nat) {
    threeven(n) implies threeven(n + 3)
} by {
    let d: Nat satisfy {
        3 * d = n
    }
    3 * (d + 1) = n + 3
}
```

--------------------------------

### Checking if an Integer is Positive in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/int.md

This snippet demonstrates the `Int.is_positive` method, which returns `Bool` indicating whether an integer is positive. It shows examples where positive numbers return true, and negative numbers or zero return false.

```Acorn
7.is_positive
not (-7).is_positive
not 0.is_positive
```

--------------------------------

### Proving threeven_everywhere with an Inline Inductive Proof in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/induction.md

This snippet illustrates an alternative inductive proof method where the base case and inductive step are integrated directly within a single theorem's proof block. The `threeven_nearby(0)` establishes the base case, and a `forall` statement handles the inductive step, demonstrating how Acorn allows for inline, anonymous proofs.

```Acorn
define threeven_nearby(n: Nat) -> Bool {
    threeven(n) or threeven(n + 1) or threeven(n + 2)
}

theorem threeven_everywhere(n: Nat) {
    threeven_nearby(n)
} by {
    // Base case
    threeven_nearby(0)

    // Inductive step
    forall(m: Nat) {
        if threeven_nearby(m) {
            if threeven(m) {
                threeven(m + 3)
                threeven_nearby(m + 1)
            } else {
                threeven(m + 1) or threeven(m + 2)
                threeven_nearby(m + 1)
            }

            // Not necessary, but here for clarity
            threeven_nearby(m + 1)
        }
    }
}
```

--------------------------------

### Defining a Basic Theorem in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/proving-a-theorem.md

This snippet defines a simple theorem named `hello_world` in Acorn. It imports the `Nat` type from the `nat` module and states that if natural number `a` is less than `b`, then `a` is not equal to `b`. This theorem is designed to be trivially provable by Acorn's AI.

```acorn
from nat import Nat

theorem hello_world(a: Nat, b: Nat) {
    a < b implies a != b
}
```

--------------------------------

### Using 'let ... satisfy' for Existential Instantiation in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/multi-step-proofs.md

This snippet demonstrates the 'let ... satisfy' construct, which is similar to 'exists' but also binds the existentially quantified variable ('d' in this case) for use in subsequent proof steps. It allows for the instantiation of an existential premise.

```acorn
let d: Nat satisfy {
    3 * d = n
}
```

--------------------------------

### Demonstrating Real Number Operators in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/real.md

This snippet illustrates the use of various operators supported by the `Real` type, including addition, multiplication, negation, and comparison. It shows how to create `Real` numbers from rationals (`Rat.0`, `Rat.1`), perform arithmetic operations like `+` and `*`, and use comparison operators like `<`, `>`, `<=`, `>=`, and equality `=`.

```Acorn
let zero: Real = Real.from_rat(Rat.0)
let one: Real = Real.from_rat(Rat.1)
let two: Real = one + one

zero < one
one > zero
zero <= zero
one >= zero

two * one = two
-(-one) = one
zero + two = two
```

--------------------------------

### Checking if a Number is Composite in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/nat.md

This snippet demonstrates the usage of the `is_composite` predicate, which determines if a given natural number is composite. According to the definition, 0 and 1 are not considered composite numbers. The example shows checking `is_composite(4)`.

```Acorn
is_composite(4)
```

--------------------------------

### Using Forall as a Multi-Step Statement in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/quantifiers.md

This snippet demonstrates how `forall` can function as a statement block, allowing multiple proof steps to be executed sequentially within its scope. The arguments are bound internally, and the final statement (`goal(a)`) is exported for use outside the block.

```acorn
forall(a: Nat) {
    step_one(a)
    step_two(a)
    step_three(a)
    goal(a)
}
```

--------------------------------

### Calculating Modulo in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/nat.md

This snippet demonstrates the `mod` function, which calculates the remainder of a division between two natural numbers. A specific definition is provided for `mod(n, 0)`, which is equal to `n`. The example shows `mod(7, 4) = 3`.

```Acorn
mod(7, 4) = 3
```

--------------------------------

### Checking if a Number is Prime in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/nat.md

This snippet illustrates the use of the `is_prime` predicate, which checks if a natural number is prime. Similar to `is_composite`, 0 and 1 are explicitly excluded from being considered prime numbers. The example shows checking `is_prime(3)`.

```Acorn
is_prime(3)
```

--------------------------------

### Adding Class Methods and Constants to LatticePoint (Acorn)

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/classes.md

This Acorn snippet demonstrates how to augment the `LatticePoint` structure with a class constant `origin` and an instance method `swap` using the `class` keyword. The `origin` constant provides a static `LatticePoint` at (0,0), while the `swap` method returns a new `LatticePoint` with its `x` and `y` coordinates exchanged. The first argument of an instance method must be named `self`.

```Acorn
class LatticePoint {
    // Now accessible as LatticePoint.origin
    let origin = LatticePoint.new(0, 0)

    // Now accessible as LatticePoint.swap
    define swap(self) -> LatticePoint {
        LatticePoint.new(self.y, self.x)
    }
}
```

--------------------------------

### Stating a Theorem Requiring Proof in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/multi-step-proofs.md

This snippet presents a theorem, 'threeven_plus_three', which states that if a number 'n' is threeven, then 'n + 3' is also threeven. This theorem is designed to illustrate a case where Acorn requires a more detailed, multi-step proof.

```acorn
theorem threeven_plus_three(n: Nat) {
    threeven(n) implies threeven(n + 3)
}
```

--------------------------------

### Importing Types from Standard Library in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/multi-step-proofs.md

This snippet shows how to import types, specifically 'Nat' (natural numbers), from standard library modules like 'nat' in Acorn. The 'from' and 'import' keywords are used to make external types available for use within the current file.

```acorn
from nat import Nat
```

--------------------------------

### Stating a Simple Theorem in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/multi-step-proofs.md

This snippet shows how to state a simple theorem in Acorn, 'zero_is_threeven', which asserts that the number zero is 'threeven'. For such straightforward theorems, Acorn can often verify them without explicit proof steps.

```acorn
theorem zero_is_threeven {
    threeven(0)
}
```

--------------------------------

### Defining an Acorn Theorem Signature

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/proving-a-theorem.md

This snippet shows the signature for an Acorn theorem named `hello_world`. It declares two parameters, `a` and `b`, both of type `Nat` (natural numbers). While theorem names are optional, they aid in code organization, and the parameters define the variables and their types used within the theorem's scope.

```acorn
theorem hello_world(a: Nat, b: Nat)
```

--------------------------------

### Declaring Unproven Theorems with `axiom` in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/experimental-stuff.md

This snippet demonstrates the `axiom` keyword in Acorn, which allows declaring a theorem as true without requiring a formal proof. This feature is noted as useful for unit testing, though its broader application might be limited.

```Acorn
axiom nat_plus_three_isnt_two(n: Nat) {
    n + 3 != 2
}

// The prover accepts this
axiom two_plus_two_is_five {
    2 + 2 = 5
}
```

--------------------------------

### Proving a Theorem about Class Method Involution (Acorn)

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/classes.md

This Acorn theorem, `swap_is_involutive`, proves that applying the `swap` method twice to a `LatticePoint` `p` returns the original point. It demonstrates how to access and use class methods on an instance (`p.swap`) and provides a proof block (`by`) detailing the coordinate transformations.

```Acorn
theorem swap_is_involutive(p: LatticePoint) {
    p.swap.swap = p
} by {
    p.swap.x = p.y
    p.swap.y = p.x
}
```

--------------------------------

### Calculating Greatest Common Divisor in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/int.md

This snippet demonstrates the `gcd` (greatest common divisor) function, which computes the greatest common divisor of two integers. It always returns a non-negative integer, as shown with examples involving positive, negative, and zero inputs.

```Acorn
gcd(6, 9) = 3
gcd(-2, -8) = 2
gcd(-3, 0) = 3
```

--------------------------------

### Using `solve` Statement for Expression Verification in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/experimental-stuff.md

This snippet illustrates the `solve` statement in Acorn, which allows for verifying mathematical expressions. The verifier checks the correctness of each statement within the block and ensures the final statement is an equality using the initial expression, though it does not check for "simplest form."

```Acorn
solve 2 + 1 by {
    2 + 1 = 3
}
```

--------------------------------

### Defining Named Functions - General Form (Acorn)

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/functions.md

This snippet illustrates the general syntax for defining named functions in Acorn using the `define` keyword. It shows how to specify function name, arguments with their types, and the return type, resulting in a function with a clearly defined signature.

```acorn
define function_name(arg1: Arg1Type, arg2: Arg2Type) -> ReturnType {
    expression
}
```

--------------------------------

### Conceptual Nat.induction Theorem Structure in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/induction.md

This snippet presents a conceptual, non-compiling representation of how a general induction theorem for natural numbers might look in Acorn. It illustrates the core components of mathematical induction: a base case (`f(0)`) and an inductive step (`forall(k: Nat) { f(k) implies f(k + 1) }`), implying the truth of `f(n)` for all `n`.

```Acorn
// This code does not actually compile, don't use it!
theorem Nat.induction(f: Nat -> Bool, n: Nat) {
    f(0) and forall(k: Nat) { f(k) implies f(k + 1) } implies f(n)
}
```

--------------------------------

### Proving Typeclass Instance Conditions Separately in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/typeclasses.md

This snippet illustrates the recommended practice of proving each condition required by a typeclass as a separate theorem before declaring the `instance`. This approach improves clarity and allows the Acorn prover to highlight specific conditions that require further proof detail, aiding in debugging.

```acorn
theorem discrete_self_distance_is_zero(x: Color) {
    discrete(x, x) = 0
}

theorem discrete_dist_zero_imp_eq(x: Color, y: Color) {
    discrete(x, y) = 0 implies x = y
}

theorem discrete_symmetric(x: Color, y: Color) {
    discrete(x, y) = discrete(y, x)
}

theorem discrete_triangle(x: Color, y: Color, z: Color) {
    discrete(x, z) <= discrete(x, y) + discrete(y, z)
}

instance Color: MetricSpace {
    let distance: (Color, Color) -> Real = discrete
}
```

--------------------------------

### Defining threeven_nearby and the threeven_everywhere Goal in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/induction.md

This code defines `threeven_nearby`, a predicate that is true if `n`, `n + 1`, or `n + 2` is a multiple of 3. It then declares the `threeven_everywhere` theorem, which states that `threeven_nearby(n)` is true for all natural numbers `n`, setting up the main induction proof goal.

```Acorn
define threeven_nearby(n: Nat) -> Bool {
    threeven(n) or threeven(n + 1) or threeven(n + 2)
}

theorem threeven_everywhere(n: Nat) {
    threeven_nearby(n)
}
```

--------------------------------

### Defining a Basic Theorem in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/basic-concepts.md

This snippet illustrates the basic structure of a theorem in Acorn. A theorem consists of a proposition to be proven (the first block) and an optional 'by' block containing the proof steps. Variables declared as arguments can be used within both blocks.

```acorn
theorem my_theorem(var1: Type1, var2: Type2, var3: Type3) {
    expression
} by {
    statement1
    statement2
    statement3
}
```

--------------------------------

### Interpreting Numerals as Natural Numbers in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/multi-step-proofs.md

This snippet demonstrates the 'numerals' keyword in Acorn, which instructs the prover to interpret literal numbers (numerals) like '3' as instances of the specified type, 'Nat' (natural numbers), for the remainder of the file.

```acorn
numerals Nat
```

--------------------------------

### Comparing Named vs. Anonymous Theorem Structures in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/induction.md

This snippet provides a direct comparison between defining a proof as a named theorem with explicit steps and achieving the same logical outcome using an anonymous `forall` statement with an `if` block. It highlights Acorn's flexibility in structuring proofs, where the last line of an `if` statement can serve as the conclusion, similar to a theorem's conclusion.

```Acorn
// Named theorem version
theorem my_theorem(x: MyType) {
    foo(x) implies bar(x)
} by {
    first_step
    second_step
}

// Same thing, but anonymous
forall(x: MyType) {
    if foo(x) {
        first_step
        second_step
        bar(x)
    }
}
```

--------------------------------

### Using Theorems as Functions for Induction (Acorn)

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/functions.md

This snippet shows how a theorem, `add_zero_left`, can be treated as a function within its own `by` block. This capability is crucial for performing inductive proofs, as it allows the theorem to be recursively called to establish properties for subsequent cases.

```acorn
theorem add_zero_left(a: Nat) {
    0 + a = a
} by {
    0 + 0 = 0
    add_zero_left(0)
    forall(x: Nat) {
        if add_zero_left(x) {
            0 + x = x
            0 + x.suc = x.suc
            add_zero_left(x.suc)
        }
    }
    add_zero_left(a)
}
```

--------------------------------

### Equivalent Forall Expression After Multi-Step Proof in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/quantifiers.md

This code shows the simplified form of a `forall` expression as it appears from outside a multi-step proof block. Even though multiple steps were involved internally, externally it is equivalent to directly proving the final goal.

```acorn
forall(a: Nat) {
    goal(a)
}
```

--------------------------------

### Mapping of Acorn Operators to Method Names (Acorn)

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/classes.md

This Acorn snippet provides a comprehensive list of supported operators and their corresponding alphabetical method names. Defining a method with one of these reserved names allows the associated operator to be used for instances of the class. This includes comparison, arithmetic, and unary negation operators.

```Acorn
// Greater than
a.gt(b) = a > b

// Less than
a.lt(b) = a < b

// Greater than or equal to
a.gte(b) = a >= b

// Less than or equal to
a.lte(b) = a <= b

// Addition
a.add(b) = a + b

// Subtraction
a.sub(b) = a - b

// Multiplication
a.mul(b) = a * b

// Division
a.div(b) = a / b

// Mod
a.mod(b) = a % b

// Negative. The unary '-' is different from the binary '-'.
a.neg = -a
```

--------------------------------

### Defining a Function Signature in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/multi-step-proofs.md

This snippet illustrates the 'define' keyword used to declare a new function named 'threeven'. It specifies that the function takes one argument, 'n', of type 'Nat' (natural number), and returns a 'Bool' (boolean) value, indicating its truth or falsehood.

```acorn
define threeven(n: Nat) -> Bool
```

--------------------------------

### Defining Functions by Satisfaction - General Form (Acorn)

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/functions.md

This general form illustrates the `let ... satisfy` statement in Acorn, which defines a function based on a condition its return value must satisfy. It includes an optional `by` block for providing a formal proof that such a return value exists.

```acorn
let function_name(arg1: Type1, arg2: Type2, ...) -> ret: ReturnType {
    expression
} by {
    proof
}
```

--------------------------------

### Executing Single GCD Step - Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/nat_gcd.md

Illustrates one step of the Euclidean algorithm, transforming a `NatPair (a, b)` into `(b, a mod b)`. This process is iterated until the second element (b) becomes zero, at which point the first element is the GCD.

```acorn
gcd_step(NatPair.new(7, 3)) = NatPair.new(3, 1)
```

--------------------------------

### Proving Identity with Overloaded Addition Operator (Acorn)

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/classes.md

This Acorn theorem, `add_origin`, demonstrates the use of the overloaded `+` operator. It proves that adding `LatticePoint.origin` (the point (0,0)) to any `LatticePoint` `p` results in `p` itself, verifying the additive identity property for `LatticePoint` instances.

```Acorn
theorem add_origin(p: LatticePoint) {
    p + LatticePoint.origin = p
}
```

--------------------------------

### Importing a Whole Module in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/imports.md

This snippet demonstrates how to import an entire module, `nat`, in Acorn. After importing, its contents like `nat.Nat` (type) and `nat.divides` (function) are accessed using dot notation. The `numerals nat.Nat` statement sets `nat.Nat` as the default type for numeric literals, and the `even_nearby` theorem proves a property about natural numbers using functions from the imported `nat` module.

```Acorn
import nat
numerals nat.Nat

theorem even_nearby(n: nat.Nat) {
  nat.divides(2, n) or nat.divides(2, n + 1)
} by {
  let (q: nat.Nat, r: nat.Nat) satisfy {
    r < 2 and n = q * 2 + r
  }
  if r = 0 {
    nat.divides(2, n)
  } else {
    r = 1
    n = q * 2 + 1
    n + 1 = (q + 1) * 2
    nat.divides(2, n + 1)
  }
}
```

--------------------------------

### Defining `bounded_sub` with Proof by Satisfaction (Acorn)

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/functions.md

This snippet defines a `bounded_sub` function that performs subtraction, returning `0` for negative results. It uses `let ... satisfy` to define the function based on a condition and includes a `by` block to provide a formal proof that a value satisfying the condition always exists.

```acorn
// This is a "bounded" version of subtraction.
// It returns 0 instead of negative numbers.
let bounded_sub(a: Nat, b: Nat) -> d: Nat satisfy {
    // The condition that `d` satisfies
    if a < b {
        d = 0
    } else {
        d + b = a
    }
} by {
    // The proof that such a `d` exists
    if a < b {
        0 = 0
    } else {
        b <= a
        let d: Nat satisfy { d + b = a }
    }
}
```

--------------------------------

### Using Existential Quantifier in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/tutorial/multi-step-proofs.md

This snippet demonstrates the 'exists' keyword, which represents the existential quantifier. It asserts that there exists some natural number 'd' such that '3 * d' equals 'n', forming the core definition of 'threeven(n)'.

```acorn
exists(d: Nat) {
    3 * d = n
}
```

--------------------------------

### Defining a `Nat` Class with `read` Function in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/experimental-stuff.md

This snippet defines a `Nat` class in Acorn, demonstrating how to implement a `read` function for processing number strings. It includes member variables for digits 0-9 and a `read` method that combines an existing number with a new digit, intended for use with `numerals` statements.

```Acorn
// Not exactly how it works in the standard library, but close
class Nat {
    let 1: Nat = Nat.0.suc
    let 2: Nat = Nat.1.suc
    let 3: Nat = Nat.2.suc
    let 4: Nat = Nat.3.suc
    let 5: Nat = Nat.4.suc
    let 6: Nat = Nat.5.suc
    let 7: Nat = Nat.6.suc
    let 8: Nat = Nat.7.suc
    let 9: Nat = Nat.8.suc

    define read(self, other: Nat) -> Nat {
        dectuple(self) + other
    }
}
```

--------------------------------

### Quantifying Over Multiple Variables in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/language/quantifiers.md

This snippet shows how to use the `exists` quantifier to bind multiple variables, `m` and `r`, simultaneously. It expresses the division algorithm for a natural number `n` by 3, stating that `n` can be written as `3 * m + r` where `r` is less than 3.

```acorn
theorem dividing_by_three(n: Nat) {
    exists(m: Nat, r: Nat) {
        3 * m + r = n and r < 3
    }
}
```

--------------------------------

### Using Natural Number Operators in Acorn

Source: https://github.com/acornprover/acornprover.org/blob/master/docs/library/nat.md

This snippet demonstrates the various arithmetic and comparison operators supported by the `Nat` type in Acorn. It shows three ways to perform addition, multiplication, subtraction (which saturates at zero), and all standard comparison operations (less than, less than or equal to, greater than, greater than or equal to). The `numerals Nat` statement enables using standard numeral syntax.

```Acorn
numerals Nat

// Three ways of adding two numbers.
2 + 2
Nat.add(2, 2)
2.add(2)

// Three ways of multiplying two numbers.
2 * 2
Nat.mul(2, 2)
2.mul(2)

// Natural number "subtraction" just stops at zero. So 1 - 2 = 0. Be careful.
4 - 2
Nat.sub(4, 2)
4.sub(2)

// Three ways for each comparison operator.
2 < 3
Nat.lt(2, 3)
2.lt(3)

2 <= 3
Nat.lte(2, 3)
2.lte(3)

5 > 4
Nat.gt(5, 4)
5.gt(4)

7 >= 0
Nat.gte(7, 0)
7.gte(0)
```