Commit 2024-07-25 22:15 e4bd83b7

View on Github →

feat: new file Data/List/Pi (#5549) The new APIs replace some definitions and lemmas in Data.FinEnum. This PR also provides more lemmas.

Estimated changes

deleted def FinEnum.Pi.cons
deleted def FinEnum.Pi.tail
deleted theorem FinEnum.mem_pi
deleted def FinEnum.pi.enum
deleted theorem FinEnum.pi.mem_enum
deleted def FinEnum.pi
added def List.Pi.enum
added theorem List.Pi.mem_enum
added theorem List.mem_pi_toList
added def List.Pi.cons
added theorem List.Pi.cons_def
added theorem List.Pi.cons_eta
added theorem List.Pi.cons_map
added def List.Pi.head
added def List.Pi.nil
added def List.Pi.tail
added theorem List.mem_pi
added def List.pi
added theorem List.pi_cons
added theorem List.pi_nil
added theorem Multiset.Pi.cons_coe
added theorem Multiset.pi_coe
modified def Multiset.Pi.cons
added theorem Multiset.Pi.cons_eta
modified theorem Multiset.Pi.cons_injective
added theorem Multiset.Pi.cons_map
modified theorem Multiset.Pi.cons_ne
modified theorem Multiset.Pi.cons_same
modified theorem Multiset.Pi.cons_swap
modified def Multiset.Pi.empty
deleted theorem Multiset.pi.cons_eta