Commit 2023-12-17 17:55 b3a1d74f

View on Github →

chore: bump Std dependency to leanprover/std4#432 (#9094) This covers these changes in Std: https://github.com/leanprover/std4/compare/6b4cf96c89e53cfcd73350bbcd90333a051ff4f0...9dd24a3493cceefa2bede383f21e4ef548990b68

Int.ofNat_natAbs_eq_of_nonneg has become Int.natAbs_of_nonneg (and one argument has become implicit)
List.map_id'' and List.map_id' have exchanged names. (Yay naming things using primes!)
Some meta functions have moved to Std and can be deleted here.

Estimated changes

Modified Mathlib/Control/Random.lean

Modified Mathlib/Data/Fintype/Card.lean

Modified Mathlib/Data/Int/ModEq.lean

Modified Mathlib/Data/List/Basic.lean

modified theorem List.map_id''

deleted theorem List.map_id'

Modified Mathlib/Data/List/BigOperators/Basic.lean

Modified Mathlib/Data/List/Sublists.lean

Modified Mathlib/Data/Nat/Squarefree.lean

Modified Mathlib/Init/Data/Int/CompLemmas.lean

Modified Mathlib/Lean/Expr/Basic.lean

deleted def Lean.Expr.int?

deleted def Lean.Expr.intLit!

deleted def Lean.Expr.nat?

deleted def Lean.Expr.natLit!

Modified Mathlib/Lean/Meta.lean

deleted def Lean.MVarId.applyConst

deleted def Lean.Meta.getLocalHyps

Modified lake-manifest.json