Theorem Primrec.list_takeWhile

Modification history

2026-03-18 02:22

Mathlib/Computability/Primrec/List.lean

feat(Computability.Primrec.List): add primrec proofs for drop, takeWhile, and dropWhile (#36473) …

Added Primrec.list_takeWhile View on Github →