Commit 2025-01-22 10:17 25190fa2

View on Github →

refactor(Data/Seq): mark Seq.recOn with cases_eliminator (#19829) Mark Seq.recOn with cases_eliminator to enable using cases tactic with sequences.

Estimated changes

Modified Mathlib/Data/Seq/Parallel.lean

Modified Mathlib/Data/Seq/Seq.lean

modified def Stream'.Seq.recOn