Commit 2022-11-05 17:02 8b889832

View on Github →

chore(data/list/count): use + 1 instead of nat.succ (#17161) Also add list.count_erase and use -1 instead of nat.pred in list.count_erase_self.

Estimated changes

Modified src/data/list/count.lean

modified theorem list.count_cons_self

added theorem list.count_erase

modified theorem list.count_erase_of_ne

modified theorem list.count_erase_self

Modified src/data/list/lattice.lean