Further reading

  • Mario Carneiro's thesis on Lean's type theory

  • Lean's official kernel: https://github.com/leanprover/lean4/tree/master/src/kernel

  • lean4lean, a reimplementation of Lean's kernel in Lean4.

  • lean4export, the recommended/official exporter for Lean 4 environments.

  • lean4checker

  • Peter Dybjer's original description of the inductive types implemented by Lean: P. Dybjer. Inductive families. Formal aspects of computing, 6(4):440–465, 1994.

  • Conor McBride and James McKinna's paper I am not a number: I am a free variable describing the locally nameless approach to bound/free variables

  • Information about non-positive occurrences in inductive types, from Counterexamples in Type Systems: https://counterexamples.org/strict-positivity.html?highlight=posi#positivity-strict-and-otherwise

  • Freek Wiedijk. Pollack-inconsistency. Electronic Notes in Theoretical Computer Science, 285:85–100, 2012