# Complete Lean examples

These source files accompany the [quantifier lesson](/learn/follow-the-scope/) and [reading reference](/reference/). They use Lean 4.28.0, have no explicit imports, and receive Lean's standard implicit `Init` import. Mathlib is not required for these files.

| File | Purpose |
| --- | --- |
| `QuantifierForallExists.lean` | Forms a proposition in which the existential choice follows the universal binder. |
| `QuantifierExistsForall.lean` | Forms a proposition with the opposite quantifier order. It supplies no proof. |
| `QuantifierProofs.lean` | Proves the first proposition and refutes the second, without axiom dependencies. |
| `RotorLaw.lean` | Supplies a record parameter with its own law field; retains an intentionally unused parameter. |
| `RecordedAxiom.lean` | Deliberately uses `sorry` to explain accepted typing and the `sorryAx` dependency. This is an unfinished proof, not an arithmetic result. |

To check a file with the matching toolchain, run `lean FileName.lean` in its directory. `RotorLaw.lean` produces an unused-variable warning. `RecordedAxiom.lean` produces a warning that the declaration uses `sorry`. The other files check without those warnings.

The files are source examples. They contain no captured editor histories, browser fixtures, or saved-record loader.