Commit 2024-03-19 17:09 e623116d

View on Github →

feat: lemmas about List.reverseRecOn (#11257) This renames the arguments to the eliminators to be more ergonomic when using the induction tactic. I also changed the definition in an attempt to make the proof easier.

Estimated changes

Modified Mathlib/Data/List/Basic.lean

modified def List.bidirectionalRec

deleted def List.bidirectionalRecOn

added theorem List.bidirectionalRec_cons_append

added theorem List.bidirectionalRec_nil

added theorem List.bidirectionalRec_singleton

modified def List.reverseRecOn

added theorem List.reverseRecOn_concat

added theorem List.reverseRecOn_nil

Modified Mathlib/Data/List/ToFinsupp.lean