Port formalized polytime to Lean - #114

Merged

rokopt merged 9 commits into

mainfrom

feat/bellantoni-cook

Aug 4, 2026

Commits on Aug 4, 2026

doc: add the Bellantoni-Cook design spec
rokopt
committed
cc77494
doc: add the Bellantoni-Cook implementation plan
rokopt
committed
480a3d6
feat(computability): add the Bellantoni-Cook signature functor
rokopt
committed
5e3fef8
feat(computability): add choice-free finiteness for the signature
rokopt
committed
6715812
feat(computability): add the Bellantoni-Cook syntax and semantics
rokopt
committed
2c5fcbb
test(computability): add worked Bellantoni-Cook expressions
rokopt
committed
f20abbb
doc: record the Bellantoni-Cook module and its follow-on work
rokopt
committed
058a494
fix: cover the successor's bit and correct three documentation notes
rokopt
committed
f153e79
doc: remove the Bellantoni-Cook spec and plan
rokopt
committed
4e6b3bd