Commit 2022-10-20 15:23 63a677d8

View on Github →

chore: update lean + std4 10-20 (#483)

Estimated changes

Modified Mathlib/Algebra/Abs.lean

Modified Mathlib/Algebra/Group/Defs.lean

Modified Mathlib/Data/Bracket.lean

Modified Mathlib/Data/Fin/Fin2.lean

Modified Mathlib/Data/List/Perm.lean

Modified Mathlib/Data/Subtype.lean

modified theorem Subtype.restrict_def

Modified Mathlib/Init/Algebra/Classes.lean

Modified Mathlib/Init/Data/Nat/Lemmas.lean

Modified Mathlib/Init/Logic.lean

modified def unexpandExistsUnique

Modified Mathlib/Init/Set.lean

Modified Mathlib/Mathport/Attributes.lean

Modified Mathlib/Mathport/Rename.lean

modified def Mathlib.Prelude.Rename.elabAlign

modified def Mathlib.Prelude.Rename.elabLookup3

Modified Mathlib/Tactic/Alias.lean

modified def Tactic.Alias.elabAlias

modified def Tactic.Alias.elabAliasLR

modified def Tactic.Alias.elabAliasLRDots

Modified Mathlib/Tactic/Basic.lean

modified def elabVariables

Modified Mathlib/Tactic/CasesM.lean

Modified Mathlib/Tactic/CommandQuote.lean

modified def Lean.Elab.Term.elabCommandQuot

modified def command.quot

Modified Mathlib/Tactic/Core.lean

Modified Mathlib/Tactic/NormCast/Tactic.lean

Modified Mathlib/Tactic/NormNum/Core.lean

Modified Mathlib/Tactic/PermuteGoals.lean

Modified Mathlib/Tactic/PrintPrefix.lean

modified def Lean.Elab.Command.elabPrintPrefix

Modified Mathlib/Tactic/Relation/Rfl.lean

Modified Mathlib/Tactic/RunCmd.lean

modified def Mathlib.RunCmd.elabRunElab

Modified Mathlib/Tactic/SimpTrace.lean

Modified Mathlib/Tactic/Simps.lean

Modified Mathlib/Tactic/ToAdditive.lean

Modified Mathlib/Util/MemoFix.lean

Modified Mathlib/Util/Time.lean

modified def timeCmdElab

Modified lakefile.lean

Modified lean-toolchain

Modified lean_packages/manifest.json