Commit 2026-03-18 02:22 f156f7ab

feat(Computability.Primrec.List): add primrec proofs for drop, takeWhile, and dropWhile (#36473) This PR adds missing proofs that several standard List operations are primitive recursive (Primrec), as well as a basic property of tail and drop. Specifically, it introduces:

• List.tail_iterate: Applying tail to a list n times is equivalent to dropping n elements.
• Primrec.list_drop: List.drop is primitive recursive.
• Primrec.list_take: List.take is primitive recursive.
• Primrec.list_takeWhile: List.takeWhile is primitive recursive.
• Primrec.list_dropWhile: List.dropWhile is primitive recursive. These are basic computability properties for lists that were currently missing from Mathlib.Computability.Primrec.List. All proofs use standard combinators and of_eq.