From cac405f4bb86f998a4d71cb6836b2a05afb4bcea Mon Sep 17 00:00:00 2001 From: Riccardo Brasca Date: Tue, 3 Jan 2023 16:22:27 +0000 Subject: [PATCH] chore: update SHA in porting header (#1306) These files correspond to files flagged "The following files have been modified since the commit at which they were verified." by `port_status.py` but are in sync with mathlib3, so we can update the hash. I only updated the easy ones, the others need a closer inspection. Co-authored-by: Reid Barton --- Mathlib/Algebra/CovariantAndContravariant.lean | 2 +- Mathlib/Algebra/Order/Group/TypeTags.lean | 2 +- Mathlib/Algebra/Order/Monoid/OrderDual.lean | 2 +- Mathlib/Algebra/Order/Monoid/Prod.lean | 2 +- Mathlib/Algebra/Order/Monoid/TypeTags.lean | 2 +- Mathlib/Algebra/Order/Monoid/WithTop.lean | 2 +- Mathlib/Combinatorics/Quiver/Push.lean | 2 +- Mathlib/Data/Int/Basic.lean | 2 +- Mathlib/Data/Nat/Order/Lemmas.lean | 2 +- Mathlib/Data/Nat/Units.lean | 2 +- Mathlib/Data/Option/NAry.lean | 2 +- Mathlib/Data/Set/NAry.lean | 2 +- Mathlib/Data/Set/Sigma.lean | 2 +- Mathlib/Order/Iterate.lean | 2 +- Mathlib/Order/Lattice.lean | 2 +- 15 files changed, 15 insertions(+), 15 deletions(-) diff --git a/Mathlib/Algebra/CovariantAndContravariant.lean b/Mathlib/Algebra/CovariantAndContravariant.lean index 1d243e92c403e..047ab2bdac19c 100644 --- a/Mathlib/Algebra/CovariantAndContravariant.lean +++ b/Mathlib/Algebra/CovariantAndContravariant.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Damiano Testa ! This file was ported from Lean 3 source module algebra.covariant_and_contravariant -! leanprover-community/mathlib commit c4658a649d216f57e99621708b09dcb3dcccbd23 +! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ diff --git a/Mathlib/Algebra/Order/Group/TypeTags.lean b/Mathlib/Algebra/Order/Group/TypeTags.lean index 84a126ce468d4..70c8cd7f790ac 100644 --- a/Mathlib/Algebra/Order/Group/TypeTags.lean +++ b/Mathlib/Algebra/Order/Group/TypeTags.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl ! This file was ported from Lean 3 source module algebra.order.group.type_tags -! leanprover-community/mathlib commit 4dc134b97a3de65ef2ed881f3513d56260971562 +! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ diff --git a/Mathlib/Algebra/Order/Monoid/OrderDual.lean b/Mathlib/Algebra/Order/Monoid/OrderDual.lean index c086ecc935b67..a98c3c352a702 100644 --- a/Mathlib/Algebra/Order/Monoid/OrderDual.lean +++ b/Mathlib/Algebra/Order/Monoid/OrderDual.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl ! This file was ported from Lean 3 source module algebra.order.monoid.order_dual -! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025 +! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ diff --git a/Mathlib/Algebra/Order/Monoid/Prod.lean b/Mathlib/Algebra/Order/Monoid/Prod.lean index 771a710511e2b..536682949772e 100644 --- a/Mathlib/Algebra/Order/Monoid/Prod.lean +++ b/Mathlib/Algebra/Order/Monoid/Prod.lean @@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl Ported by: Joël Riou ! This file was ported from Lean 3 source module algebra.order.monoid.prod -! leanprover-community/mathlib commit fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e +! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ diff --git a/Mathlib/Algebra/Order/Monoid/TypeTags.lean b/Mathlib/Algebra/Order/Monoid/TypeTags.lean index 443a84680322c..7b2ac263ea5de 100644 --- a/Mathlib/Algebra/Order/Monoid/TypeTags.lean +++ b/Mathlib/Algebra/Order/Monoid/TypeTags.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl ! This file was ported from Lean 3 source module algebra.order.monoid.type_tags -! leanprover-community/mathlib commit f1a2caaf51ef593799107fe9a8d5e411599f3996 +! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ diff --git a/Mathlib/Algebra/Order/Monoid/WithTop.lean b/Mathlib/Algebra/Order/Monoid/WithTop.lean index 6f9987c994b61..4468ebf3cd396 100644 --- a/Mathlib/Algebra/Order/Monoid/WithTop.lean +++ b/Mathlib/Algebra/Order/Monoid/WithTop.lean @@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Johannes Hölzl Ported by: Jon Eugster ! This file was ported from Lean 3 source module algebra.order.monoid.with_top -! leanprover-community/mathlib commit 655994e298904d7e5bbd1e18c95defd7b543eb94 +! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ diff --git a/Mathlib/Combinatorics/Quiver/Push.lean b/Mathlib/Combinatorics/Quiver/Push.lean index 50ce529a89fb6..1c771c722c1d8 100644 --- a/Mathlib/Combinatorics/Quiver/Push.lean +++ b/Mathlib/Combinatorics/Quiver/Push.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Rémi Bottinelli ! This file was ported from Lean 3 source module combinatorics.quiver.push -! leanprover-community/mathlib commit 9b2660e1b25419042c8da10bf411aa3c67f14383 +! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ diff --git a/Mathlib/Data/Int/Basic.lean b/Mathlib/Data/Int/Basic.lean index 1a4f13e69c085..9e435a4ecd526 100644 --- a/Mathlib/Data/Int/Basic.lean +++ b/Mathlib/Data/Int/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad ! This file was ported from Lean 3 source module data.int.basic -! leanprover-community/mathlib commit a148d797a1094ab554ad4183a4ad6f130358ef64 +! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ diff --git a/Mathlib/Data/Nat/Order/Lemmas.lean b/Mathlib/Data/Nat/Order/Lemmas.lean index f4ae935bb2815..da8f7ab666728 100644 --- a/Mathlib/Data/Nat/Order/Lemmas.lean +++ b/Mathlib/Data/Nat/Order/Lemmas.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro ! This file was ported from Lean 3 source module data.nat.order.lemmas -! leanprover-community/mathlib commit 10b4e499f43088dd3bb7b5796184ad5216648ab1 +! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ diff --git a/Mathlib/Data/Nat/Units.lean b/Mathlib/Data/Nat/Units.lean index e7d5863c725f4..a21a402c164dc 100644 --- a/Mathlib/Data/Nat/Units.lean +++ b/Mathlib/Data/Nat/Units.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad, Mario Carneiro ! This file was ported from Lean 3 source module data.nat.units -! leanprover-community/mathlib commit 70d50ecfd4900dd6d328da39ab7ebd516abe4025 +! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ diff --git a/Mathlib/Data/Option/NAry.lean b/Mathlib/Data/Option/NAry.lean index 9684039d4c7d9..3037184a51b71 100644 --- a/Mathlib/Data/Option/NAry.lean +++ b/Mathlib/Data/Option/NAry.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies ! This file was ported from Lean 3 source module data.option.n_ary -! leanprover-community/mathlib commit d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d +! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ diff --git a/Mathlib/Data/Set/NAry.lean b/Mathlib/Data/Set/NAry.lean index b11553fdd40b5..b4228c6682ca8 100644 --- a/Mathlib/Data/Set/NAry.lean +++ b/Mathlib/Data/Set/NAry.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn ! This file was ported from Lean 3 source module data.set.n_ary -! leanprover-community/mathlib commit cf9386b56953fb40904843af98b7a80757bbe7f9 +! leanprover-community/mathlib commit d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ diff --git a/Mathlib/Data/Set/Sigma.lean b/Mathlib/Data/Set/Sigma.lean index 1bf3803bb39bc..8bfd12799b3be 100644 --- a/Mathlib/Data/Set/Sigma.lean +++ b/Mathlib/Data/Set/Sigma.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yaël Dillies ! This file was ported from Lean 3 source module data.set.sigma -! leanprover-community/mathlib commit fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e +! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ diff --git a/Mathlib/Order/Iterate.lean b/Mathlib/Order/Iterate.lean index 77e57de074515..ad0746a2dea4a 100644 --- a/Mathlib/Order/Iterate.lean +++ b/Mathlib/Order/Iterate.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Yury G. Kudryashov ! This file was ported from Lean 3 source module order.iterate -! leanprover-community/mathlib commit d6aae1bcbd04b8de2022b9b83a5b5b10e10c777d +! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ diff --git a/Mathlib/Order/Lattice.lean b/Mathlib/Order/Lattice.lean index 5d2eccc14ef21..ac70f87346621 100644 --- a/Mathlib/Order/Lattice.lean +++ b/Mathlib/Order/Lattice.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl ! This file was ported from Lean 3 source module order.lattice -! leanprover-community/mathlib commit a148d797a1094ab554ad4183a4ad6f130358ef64 +! leanprover-community/mathlib commit 2258b40dacd2942571c8ce136215350c702dc78f ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/