Commit 2023-06-09 00:56 93207147

View on Github →

chore: bump lean 06-07 (#4849)

Estimated changes

Modified Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

Modified Mathlib/Analysis/NormedSpace/Multilinear.lean

Modified Mathlib/Tactic/Have.lean

deleted def Lean.Parser.Term.haveIdLhs'

added def Mathlib.Tactic.haveIdLhs'

modified def Mathlib.Tactic.haveLetCore

added def Mathlib.Tactic.hygieneInfo

added def Mathlib.Tactic.hygieneInfoFn

added def Mathlib.Tactic.hygieneInfoNoAntiquot.formatter

added def Mathlib.Tactic.hygieneInfoNoAntiquot.parenthesizer

added def Mathlib.Tactic.hygieneInfoNoAntiquot

added def Mathlib.Tactic.optBinderIdent.name

added def Mathlib.Tactic.optBinderIdent

Modified Mathlib/Tactic/Replace.lean

Modified lake-manifest.json

Modified lean-toolchain

Modified test/Have.lean

Modified test/wlog.lean