Commit 2024-06-08 10:13 8462800a

View on Github →

chore(Data/List): cleanup redundant type arguments (#13605)

Estimated changes

modified theorem List.getLast_pmap
modified theorem List.injective_foldl_comp
modified theorem List.intersperse_cons_cons
modified theorem List.intersperse_singleton
modified theorem List.mem_pure
modified theorem List.pmap_append'
modified theorem List.splitOn_nil
modified theorem List.count_map_of_injective
modified theorem List.nodup_ofFn
modified theorem List.nodup_ofFn_ofInjective
modified theorem List.ofFn_eq_map
modified theorem List.ofFn_eq_pmap
modified theorem List.length_mapIdx
modified def List.mapIdxMAuxSpec
modified theorem List.mapIdxMAuxSpec_cons
modified theorem List.mapIdxM_eq_mmap_enum
modified theorem List.mapIdx_append
modified theorem List.mapIdx_cons
modified theorem List.mapIdx_eq_nil
modified theorem List.mapIdx_eq_ofFn
modified theorem List.nthLe_mapIdx
modified theorem Option.toList_nodup
modified theorem List.Perm.dropSlice_inter
modified theorem List.Perm.drop_inter
modified theorem List.Perm.take_inter
modified theorem List.map_permutationsAux2'
modified theorem List.zipWith_rotate_distrib
modified theorem List.sizeOf_dedupKeys
modified theorem List.sizeOf_kerase
modified theorem List.length_of_sublistsLen
modified theorem List.length_sublistsLen
modified theorem List.mem_sublistsLen
modified theorem List.mem_sublistsLen_self
modified def List.sublistsLen
modified def List.sublistsLenAux
modified theorem List.sublistsLenAux_append
modified theorem List.sublistsLenAux_eq
modified theorem List.sublistsLenAux_zero
modified theorem List.sublistsLen_one
modified theorem List.sublistsLen_succ_cons
modified theorem List.sublistsLen_succ_nil
modified theorem List.sublistsLen_zero
modified theorem List.get?_zip_with_eq_some