Lean examples
These complete files accompany Reading mathematics with Definograph. Each runs independently with Lean 4.28.0, using the implicit standard Init import. No mathlib or other package is required.
Run lean FileName.lean with the matching toolchain. Some files deliberately produce informational output or warnings:
| File | Purpose | Expected result |
|---|---|---|
| Scope.lean | Compare quantifier order and variable names. | Each #check expression has type Prop; both proposition-forming declarations are accepted. The constant-choice example has an expected unused-variable warning for x. |
| QuantifierForallExists.lean | Exact first source for the optional editor activity. | Accepted proposition-forming declaration. |
| QuantifierExistsForall.lean | Exact second source for the optional editor activity. | Accepted proposition-forming declaration; this does not prove its proposition. |
| QuantifierProofs.lean | Prove the first proposition and refute the second. | Both theorems report no axiom dependencies. |
| RotorLaw.lean | Inspect a record owner and its law. | Accepted, with an expected unused-variable warning. |
| RotorExamples.lean | Construct natural-number and empty-carrier records; apply an owned law. | Accepted; the named definitions and theorem report no axiom dependencies. |
| Evidence.lean | Compare a local hypothesis with a placeholder dependency. | from_hypothesis reports no axiom dependencies; claimed produces a sorry warning and depends on sorryAx. |
| ReturnMap.lean | Read an unfamiliar law, check a counterexample to its converse, and prove injectivity. | Accepted, with an expected unused-variable warning; the named checked definitions/theorems report no axiom dependencies. |
Rotor is declared independently in its two files so each can be read and run alone. Run the files individually instead of pasting all downloads into one namespace.
Lean compilation checks the sources. It does not establish that every example has a guided Definograph presentation; the lessons state where an editor workflow is documented and where an example is a new inspection exercise.