Commit 2024-12-02 04:16 41ff1f78

View on Github →

chore: bump toolchain to v4.15.0-rc1, and merge bump/v4.15.0 adaptations branch (#19675)

Estimated changes

deleted def Miu.Miustr
modified theorem Finset.pow_subset_pow_left
modified def Nat.Partrec'.Vec
modified theorem Nat.Partrec'.comp₁
modified theorem Nat.Partrec'.of_eq
modified theorem Nat.Partrec'.of_prim
modified theorem Nat.Partrec'.rfindOpt
modified inductive Nat.Partrec'
modified theorem Computable.vector_cons
modified theorem Computable.vector_get
modified theorem Computable.vector_head
modified theorem Computable.vector_length
modified theorem Computable.vector_ofFn'
modified theorem Computable.vector_tail
modified theorem Computable.vector_toList
modified def Nat.Primrec'.Vec
modified theorem Nat.Primrec'.of_eq
modified inductive Nat.Primrec'
modified theorem Primrec.vector_cons
modified theorem Primrec.vector_get'
modified theorem Primrec.vector_get
modified theorem Primrec.vector_head
modified theorem Primrec.vector_length
modified theorem Primrec.vector_ofFn'
modified theorem Primrec.vector_tail
modified theorem Primrec.vector_toList
modified theorem Primrec.vector_toList_iff
modified def Turing.TM1to1.readAux
added theorem Finset.subset_of_le
modified theorem card_vector
modified theorem List.get?_length
modified theorem List.getElem?_length
added theorem List.getLast_filter'
deleted theorem List.getLast_filter
modified theorem List.take_concat_get'
modified theorem List.mapIdx_append_one
deleted theorem List.eraseIdx_insertIdx
deleted theorem List.insertIdx_comm
deleted theorem List.insertIdx_succ_cons
deleted theorem List.insertIdx_succ_nil
deleted theorem List.insertIdx_zero
deleted theorem List.length_insertIdx
deleted theorem List.mem_insertIdx
deleted theorem List.getLast_ofFn
deleted theorem List.head_ofFn
deleted theorem List.ofFn_eq_nil_iff
deleted theorem List.ofFn_succ
deleted theorem List.ofFn_zero
deleted theorem Nat.lt_pow_self
deleted theorem Nat.lt_two_pow
modified def SNum.bits
modified theorem Sym.cons_of_coe_eq
modified def Sym.ofVector
modified theorem Sym.ofVector_cons
modified theorem Sym.ofVector_nil
modified theorem Sym.sound
modified theorem Mathlib.Vector.get_mem
modified theorem Cardinal.mk_vector
modified structure TopCat.GlueData
modified theorem Vector.continuous_insertIdx
modified theorem Vector.tendsto_cons
modified structure UnderScoreDigit.Prod