Reservoir

No results found
All Packages

partial-combinatory-algebras

A Lean 4 formalization of partial combinatory algebras.
  • Readme
  • Versions (1)
  • Dependencies (14)

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
  • MIT
  • 8 days ago
    Last updated on June 23, 2025 at 12:53:17AM
  • 14 stars

Lean

  • Commit 8a97af1 fails to build on leanprover/lean4:v4.15.0-rc1
    v4.15.0-rc1
  • Commit 73418c6 builds on the old leanprover/lean4:v4.14.0
    v4.14.0
  • Commit b61ac10 builds on the old leanprover/lean4:v4.14.0-rc3
    v4.14.0-rc3
  • Commit b49123f builds on the old leanprover/lean4:v4.14.0-rc2
    v4.14.0-rc2
  • Commit b61ac10 builds on the old leanprover/lean4:v4.13.0
    v4.13.0
  • 17 more

Repository

andrejbauer/partial-combinatory-algebras

About

  • lean-lang.org
  • The Lean FRO
  • Terms of Use
  • Privacy Policy

Explore

  • Games
  • Playground
  • Community
  • Moogle
  • Loogle

Learn

  • The Lean Manual
  • Theorem Proving in Lean
  • Functional Programming in Lean
  • Mathematics in Lean
  • The Mechanics of Proof
  • How To Prove It With Lean

Social

  • leanprover
  • @leanprover
  • Lean FRO
  • leanprover