chore: bump to 2023-01-04 (#1335)

leanprover-community · Jan 4, 2023 · 7e2613a · 7e2613a
1 parent 047e52a
commit 7e2613a
Show file tree

Hide file tree

Showing 36 changed files with 6 additions and 92 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -593,7 +593,6 @@ import Mathlib.Testing.SlimCheck.Sampleable
 import Mathlib.Testing.SlimCheck.Testable
 import Mathlib.Util.Export
 import Mathlib.Util.IncludeStr
-import Mathlib.Util.MapsTo
 import Mathlib.Util.MemoFix
 import Mathlib.Util.Simp
 import Mathlib.Util.Syntax

diff --git a/Mathlib/Control/Functor.lean b/Mathlib/Control/Functor.lean
@@ -10,6 +10,7 @@ Authors: Simon Hudon
 -/
 import Mathlib.Control.Basic
 import Mathlib.Init.Set
+import Std.Tactic.Lint
 
 /-!
 # Functors

diff --git a/Mathlib/Data/KVMap.lean b/Mathlib/Data/KVMap.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex J. Best
 -/
 import Lean.Data.KVMap
-import Mathlib.Util.MapsTo
 
 /-!
 # Additional functionality for `KVMap`

diff --git a/Mathlib/Init/Data/Fin/Basic.lean b/Mathlib/Init/Data/Fin/Basic.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Mathlib.Init.Data.Nat.Notation
-import Mathlib.Util.MapsTo
 
 /-!
 # Theorems about equality in `Fin`.

diff --git a/Mathlib/Init/Set.lean b/Mathlib/Init/Set.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Parser.Term
-import Mathlib.Util.MapsTo
 import Std.Classes.SetNotation
 import Mathlib.Mathport.Rename
 

diff --git a/Mathlib/Lean/Expr/Basic.lean b/Mathlib/Lean/Expr/Basic.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro, Simon Hudon, Scott Morrison, Keeley Hoek, Robert Y. Lew
 Floris van Doorn, E.W.Ayers, Arthur Paulino
 -/
 import Lean
-import Mathlib.Util.MapsTo
 import Std.Lean.Expr
 import Std.Data.List.Basic
 

diff --git a/Mathlib/Lean/Meta.lean b/Mathlib/Lean/Meta.lean
@@ -6,7 +6,6 @@ Authors: Mario Carneiro
 import Lean.Elab
 import Lean.Meta.Tactic.Assert
 import Lean.Meta.Tactic.Clear
-import Mathlib.Util.MapsTo
 
 /-! ## Additional utilities in `Lean.MVarId` -/
 

diff --git a/Mathlib/Mathport/Rename.lean b/Mathlib/Mathport/Rename.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Daniel Selsam
 -/
 import Lean
-import Mathlib.Util.MapsTo
 
 namespace Mathlib.Prelude.Rename
 

diff --git a/Mathlib/Order/Antichain.lean b/Mathlib/Order/Antichain.lean
@@ -338,7 +338,7 @@ variable {ι : Type _} {α : ι → Type _} [∀ i, Preorder (α i)] {s t : Set
 
 -- Porting note: local notation given a name because of https://github.com/leanprover/lean4/issues/2000
 @[inherit_doc]
-local infixl:50 (name := «OrderAntichainLocal≺») " ≺ " => StrongLT
+local infixl:50 " ≺ " => StrongLT
 
 /-- A weak antichain in `Π i, α i` is a set such that no two distinct elements are strongly less
 than each other. -/

diff --git a/Mathlib/Order/Chain.lean b/Mathlib/Order/Chain.lean
@@ -45,7 +45,7 @@ variable (r : α → α → Prop)
 
 /-- In this file, we use `≺` as a local notation for any relation `r`. -/
 -- Porting note: local notation given a name because of https://github.com/leanprover/lean4/issues/2000
-local infixl:50 (name := «OrderChainLocal≺») " ≺ " => r
+local infixl:50 " ≺ " => r
 
 /-- A chain is a set `s` satisfying `x ≺ y ∨ x = y ∨ y ≺ x` for all `x y ∈ s`. -/
 def IsChain (s : Set α) : Prop :=

diff --git a/Mathlib/Order/Zorn.lean b/Mathlib/Order/Zorn.lean
@@ -72,7 +72,7 @@ variable {α β : Type _} {r : α → α → Prop} {c : Set α}
 
 /-- Local notation for the relation being considered. -/
 -- Porting note: local notation given a name because of https://github.com/leanprover/lean4/issues/2000
-local infixl:50 (name := «OrderZornLocal≺») " ≺ " => r
+local infixl:50 " ≺ " => r
 
 /-- **Zorn's lemma**
 

diff --git a/Mathlib/Tactic/Alias.lean b/Mathlib/Tactic/Alias.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, David Renshaw
 -/
 import Lean
-import Mathlib.Util.MapsTo
 
 /-!
 # The `alias` command

diff --git a/Mathlib/Tactic/ApplyRules.lean b/Mathlib/Tactic/ApplyRules.lean
@@ -6,7 +6,6 @@ Authors: Scott Morrison
 import Lean
 import Std.Util.TermUnsafe
 import Std.Lean.Meta.Basic
-import Mathlib.Util.MapsTo
 
 /-!
 # The `apply_rules` tactic

diff --git a/Mathlib/Tactic/Basic.lean b/Mathlib/Tactic/Basic.lean
@@ -6,7 +6,6 @@ Authors: Mario Carneiro
 import Lean
 import Std
 import Mathlib.Tactic.Cases
-import Mathlib.Util.MapsTo
 
 namespace Mathlib.Tactic
 open Lean Parser.Tactic Elab Command Elab.Tactic Meta

diff --git a/Mathlib/Tactic/CasesM.lean b/Mathlib/Tactic/CasesM.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Lean
-import Mathlib.Util.MapsTo
 
 /-!
 # `casesm`, `cases_type`, `constructorm` tactics

diff --git a/Mathlib/Tactic/Clear!.lean b/Mathlib/Tactic/Clear!.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joshua Clune
 -/
 import Lean
-import Mathlib.Util.MapsTo
 
 /-! # `clear!` tactic -/
 

diff --git a/Mathlib/Tactic/ClearExcept.lean b/Mathlib/Tactic/ClearExcept.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joshua Clune
 -/
 import Lean
-import Mathlib.Util.MapsTo
 
 open Lean.Meta
 

diff --git a/Mathlib/Tactic/Clear_.lean b/Mathlib/Tactic/Clear_.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joshua Clune
 -/
 import Lean
-import Mathlib.Util.MapsTo
 
 /-! # `clear_` tactic -/
 

diff --git a/Mathlib/Tactic/Coe.lean b/Mathlib/Tactic/Coe.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
 import Lean
-import Mathlib.Util.MapsTo
 
 open Lean Elab Term Meta
 

diff --git a/Mathlib/Tactic/Convert.lean b/Mathlib/Tactic/Convert.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import Lean
-import Mathlib.Util.MapsTo
 
 /-!
 # The `convert` tactic.

diff --git a/Mathlib/Tactic/Have.lean b/Mathlib/Tactic/Have.lean
@@ -5,7 +5,6 @@ Authors: Arthur Paulino, Edward Ayers, Mario Carneiro
 -/
 import Lean
 import Mathlib.Data.Array.Defs
-import Mathlib.Util.MapsTo
 
 /--
 Uses `checkColGt` to prevent

diff --git a/Mathlib/Tactic/IrreducibleDef.lean b/Mathlib/Tactic/IrreducibleDef.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
 import Lean
-import Mathlib.Util.MapsTo
 
 /-!
 # Irreducible definitions

diff --git a/Mathlib/Tactic/LeftRight.lean b/Mathlib/Tactic/LeftRight.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Siddhartha Gadgil
 -/
 import Lean
-import Mathlib.Util.MapsTo
 
 namespace Mathlib.Tactic.LeftRight
 open Lean Meta Elab Tactic

diff --git a/Mathlib/Tactic/PrintPrefix.lean b/Mathlib/Tactic/PrintPrefix.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shing Tak Lam, Daniel Selsam, Mario Carneiro
 -/
 import Lean.Elab.Command
-import Mathlib.Util.MapsTo
 
 open Lean Meta Elab Command
 

diff --git a/Mathlib/Tactic/Relation/Rfl.lean b/Mathlib/Tactic/Relation/Rfl.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Newell Jensen
 -/
 import Lean
-import Mathlib.Util.MapsTo
 
 /-!
 # `rfl` tactic extension for reflexive relations

diff --git a/Mathlib/Tactic/Rename.lean b/Mathlib/Tactic/Rename.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
 import Lean
-import Mathlib.Util.MapsTo
 
 namespace Mathlib.Tactic
 

diff --git a/Mathlib/Tactic/RunCmd.lean b/Mathlib/Tactic/RunCmd.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sebastian Ullrich, Mario Carneiro
 -/
 import Lean.Elab.Eval
-import Mathlib.Util.MapsTo
 import Std.Util.TermUnsafe
 
 /-!

diff --git a/Mathlib/Tactic/Set.lean b/Mathlib/Tactic/Set.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ian Benway.
 -/
 import Lean
-import Mathlib.Util.MapsTo
 
 namespace Mathlib.Tactic
 open Lean Elab Elab.Tactic Meta

diff --git a/Mathlib/Tactic/SimpIntro.lean b/Mathlib/Tactic/SimpIntro.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Lean
 import Std.Lean.Parser
-import Mathlib.Util.MapsTo
 
 /-! # `simp_intro` tactic -/
 

diff --git a/Mathlib/Tactic/SudoSetOption.lean b/Mathlib/Tactic/SudoSetOption.lean
@@ -5,7 +5,6 @@ Authors: Gabriel Ebner
 -/
 
 import Lean
-import Mathlib.Util.MapsTo
 
 /-!
 # Defines the `sudo set_option` command.

diff --git a/Mathlib/Tactic/ToAdditive.lean b/Mathlib/Tactic/ToAdditive.lean
@@ -16,6 +16,7 @@ import Mathlib.Tactic.Relation.Rfl -- just to copy the attribute
 import Mathlib.Tactic.Relation.Symm -- just to copy the attribute
 import Mathlib.Tactic.Relation.Trans -- just to copy the attribute
 import Mathlib.Tactic.RunCmd -- not necessary, but useful for debugging
+import Std.Tactic.Lint.Simp -- for DiscrTree.elements
 
 /-!
 # The `@[to_additive]` attribute.

diff --git a/Mathlib/Util/Export.lean b/Mathlib/Util/Export.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 import Lean
-import Mathlib.Util.MapsTo
 
 /-!
 A rudimentary export format, adapted from

diff --git a/Mathlib/Util/MapsTo.lean b/Mathlib/Util/MapsTo.lean
diff --git a/Mathlib/Util/Simp.lean b/Mathlib/Util/Simp.lean
@@ -6,7 +6,6 @@ Authors: Gabriel Ebner
 
 import Lean
 import Std.Tactic.OpenPrivate
-import Mathlib.Util.MapsTo
 
 /-!
 # Helper functions for the `norm_cast` tactic.

diff --git a/Mathlib/Util/WithWeakNamespace.lean b/Mathlib/Util/WithWeakNamespace.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro, Daniel Selsam, Gabriel Ebner
 -/
 
 import Lean
-import Mathlib.Util.MapsTo
 
 /-!
 # Defines `with_weak_namespace` command.

diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2022-12-23
+leanprover/lean4:nightly-2023-01-04