Commit 2024-06-06 13:05 149b6c3f
View on Github →feat(Computability/Primrec): recursion on order type omega is primitive recursive (#8619)
add Primrec.nat_omega_rec, which states that function defined recursively on order type omega is primitive recursive, and is stronger than Primrec.nat_strong_rec. also add some basic theorems about List