Commit 2025-08-16 00:05 b2b88d76
View on Github →feat: filtering lists and bounded quantifiers are primitive recursive (#26295) A few useful lemmas not explicitly in Primrec.lean :
- Filtering for elements from a list that meet a primrec criterion is primrec
- Checking whether a list has some element meeting a primrec criterion is primrec
- Checking whether every element of a list meets a primrec criterion is primrec
- Primitive recursive functions are closed under bounded existential and universal quantifiers