Commit 2024-11-04 05:59 a7fc949f

View on Github →

chore: bump toolchain to v4.14.0-rc1 (#18597)

  • This needs #18591 merged first.

Estimated changes

deleted theorem List.countP_bind
added theorem List.countP_flatMap
deleted theorem List.count_bind
added theorem List.count_flatMap
added theorem List.drop_sum_flatten
deleted theorem List.drop_sum_join
deleted theorem List.length_bind
added theorem List.length_flatMap
modified theorem List.prod_cons
added theorem List.prod_flatten
deleted theorem List.prod_join
added theorem List.ranges_flatten
deleted theorem List.ranges_join
added theorem List.ranges_nodup
added theorem List.take_sum_flatten
deleted theorem List.take_sum_join
modified theorem Nat.sum_eq_listSum
deleted theorem FreeMonoid.ofList_join
modified theorem FreeMonoid.toList_prod
modified theorem Language.join_mem_kstar
modified theorem Language.kstar_def
modified theorem Language.mem_kstar
deleted theorem Primrec.list_bind
added theorem Primrec.list_flatMap
added theorem Primrec.list_flatten
deleted theorem Primrec.list_join
deleted theorem Turing.ListBlank.bind_mk
added theorem BitVec.ofFin_intCast
added theorem BitVec.ofFin_natCast
added theorem BitVec.ofFin_neg
added theorem BitVec.toFin_intCast
added theorem BitVec.toFin_natCast
deleted theorem List.bind_congr
deleted theorem List.bind_eq_bind
added theorem List.bind_eq_flatMap
deleted theorem List.bind_pure_eq_map
added theorem List.flatMap_congr
deleted theorem List.infix_bind_of_mem
deleted theorem List.modify_eq_set
added theorem List.chain'_flatten
deleted theorem List.chain'_join
deleted theorem List.rel_bind
added theorem List.rel_flatMap
added theorem List.rel_flatten
deleted theorem List.rel_join
deleted theorem List.groupBy_nil
deleted theorem List.join_groupBy
deleted theorem List.nil_not_mem_groupBy
deleted theorem List.getElem?_mapIdx
deleted theorem List.getElem?_mapIdx_go
deleted theorem List.length_mapIdx
deleted theorem List.length_mapIdx_go
deleted theorem List.mapIdxGo_append
deleted theorem List.mapIdxGo_length
deleted theorem List.mapIdx_append
deleted theorem List.mapIdx_cons
deleted theorem List.mapIdx_eq_enum_map
deleted theorem List.mapIdx_eq_nil
deleted theorem List.mapIdx_nil
deleted theorem List.countP_bind'
added theorem List.countP_flatMap'
added theorem List.countP_flatten'
deleted theorem List.countP_join'
deleted theorem List.count_bind'
added theorem List.count_flatMap'
added theorem List.count_flatten'
deleted theorem List.count_join'
added theorem List.drop_sum_flatten'
deleted theorem List.drop_sum_join'
deleted theorem List.length_bind'
added theorem List.length_flatMap'
added theorem List.length_flatten'
deleted theorem List.length_join'
added theorem List.sublist_join
added theorem List.take_sum_flatten'
deleted theorem List.take_sum_join'
deleted theorem List.nodup_bind
added theorem List.nodup_flatMap
added theorem List.nodup_flatten
deleted theorem List.nodup_join
deleted theorem List.Perm.bind_left
added theorem List.Perm.flatMap_left
deleted theorem List.bind_append_perm
deleted theorem List.map_append_bind_perm
added theorem List.ranges_flatten'
deleted theorem List.ranges_join'
deleted theorem List.ranges_nodup
added theorem List.nodupKeys_flatten
deleted theorem List.nodupKeys_join
added theorem List.flatten_splitBy
added theorem List.splitBy_nil
deleted theorem List.sublistsAux_eq_bind
modified theorem Multiset.coe_bind
modified theorem Multiset.coe_join
deleted theorem Prod.fst_swap
deleted theorem Prod.map_comp_map
deleted theorem Prod.map_comp_swap
deleted theorem Prod.map_id'
deleted theorem Prod.map_id
deleted theorem Prod.map_map
deleted theorem Prod.snd_swap
deleted def Prod.swap
deleted theorem Prod.swap_inj
deleted theorem Prod.swap_prod_mk
deleted theorem Prod.swap_swap
deleted theorem Prod.swap_swap_eq
modified theorem $typeName.neg_def
modified theorem $typeName.nsmul_def
modified theorem $typeName.pow_def
modified theorem $typeName.zsmul_def
modified def UInt8.toChar
modified theorem FreeGroup.pow_mk
deleted theorem pi_congr
deleted theorem Function.curry_apply
deleted def Function.curry
deleted theorem Function.curry_uncurry
deleted def Function.uncurry
deleted theorem Function.uncurry_curry
modified inductive tests.C'
modified inductive tests.D
modified def Equiv'.trans
modified def myNatEquiv
modified def myTypeDef