A Lean 4 formalization of partial combinatory algebras which serves as a model project for the course Formalized mathematics and proof assistants, taught in the Fall of 2024 by Andrej Bauer at the Faculty of mathematics and physics, University of Ljubljana.

Please consult:

• Blueprint
• Blueprint as pdf
• Dependency graph
• Doc pages for this repository