Partial combinatory algebras

See the license file for copyright information.

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.

Further information is available at the project web pages:

• blueprint
• documentation