Skip to content

Commit 11763e7

Browse files
kim-emclaude
kim-em
and
claude
committed
chore: add module keyword to Archive and Counterexamples files
This PR converts 105 Archive and Counterexamples files to module format, adding `module`, `public import`, and `@[expose] public section`. Eight files are left unconverted for now: - Seven files containing `private` declarations that need further work - `Counterexamples/InvertibleModuleNotIdeal` which needs an import path update Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
1 parent 9036ce5 commit 11763e7

105 files changed

Lines changed: 748 additions & 332 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎Archive/Arithcc.lean‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,15 @@
1+
module
12
/-
23
Copyright (c) 2020 Xi Wang. All rights reserved.
34
Released under Apache 2.0 license as described in the file LICENSE.
45
Authors: Xi Wang
56
-/
6-
import Mathlib.Data.Nat.Basic
7-
import Mathlib.Order.Basic
8-
import Mathlib.Tactic.Common
7+
public import Mathlib.Data.Nat.Basic
8+
public import Mathlib.Order.Basic
9+
public import Mathlib.Tactic.Common
10+
11+
12+
@[expose] public section
913

1014
/-!
1115
# A compiler for arithmetic expressions

‎Archive/Examples/Eisenstein.lean‎

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,19 @@
1+
module
12
/-
23
Copyright (c) 2025 Antoine Chambert-Loir. All rights reserved.
34
Released under Apache 2.0 license as described in the file LICENSE.
45
Authors: Antoine Chambert-Loir
56
-/
67

7-
import Mathlib.Algebra.CharP.Quotient
8-
import Mathlib.Algebra.Field.ZMod
9-
import Mathlib.Algebra.Polynomial.SpecificDegree
10-
import Mathlib.RingTheory.Ideal.Quotient.Operations
11-
import Mathlib.RingTheory.Polynomial.Eisenstein.Basic
12-
import Mathlib.Tactic.ComputeDegree
8+
public import Mathlib.Algebra.CharP.Quotient
9+
public import Mathlib.Algebra.Field.ZMod
10+
public import Mathlib.Algebra.Polynomial.SpecificDegree
11+
public import Mathlib.RingTheory.Ideal.Quotient.Operations
12+
public import Mathlib.RingTheory.Polynomial.Eisenstein.Basic
13+
public import Mathlib.Tactic.ComputeDegree
14+
15+
16+
@[expose] public section
1317

1418
/-! # Example of an application of the generalized Eisenstein criterion
1519

‎Archive/Examples/IfNormalization/Result.lean‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,15 @@
1+
module
12
/-
23
Copyright (c) 2023 Chris Hughes. All rights reserved.
34
Released under Apache 2.0 license as described in the file LICENSE.
45
Authors: Chris Hughes
56
-/
6-
import Archive.Examples.IfNormalization.Statement
7-
import Mathlib.Data.List.AList
8-
import Mathlib.Tactic.Recall
7+
public import Archive.Examples.IfNormalization.Statement
8+
public import Mathlib.Data.List.AList
9+
public import Mathlib.Tactic.Recall
10+
11+
12+
@[expose] public section
913

1014
/-!
1115
# A solution to the if normalization challenge in Lean.

‎Archive/Examples/IfNormalization/Statement.lean‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,12 @@
1+
module
12
/-
23
Copyright (c) 2023 Lean FRO LLC. All rights reserved.
34
Released under Apache 2.0 license as described in the file LICENSE.
45
Authors: Kim Morrison
56
-/
67

8+
@[expose] public section
9+
710
/-!
811
# If normalization
912

‎Archive/Examples/IfNormalization/WithoutAesop.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,14 @@
1+
module
12
/-
23
Copyright (c) 2023 Chris Hughes. All rights reserved.
34
Released under Apache 2.0 license as described in the file LICENSE.
45
Authors: Chris Hughes, Kim Morrison
56
-/
6-
import Archive.Examples.IfNormalization.Statement
7-
import Mathlib.Data.List.AList
7+
public import Archive.Examples.IfNormalization.Statement
8+
public import Mathlib.Data.List.AList
9+
10+
11+
@[expose] public section
812

913
/-!
1014
# A variant of Chris Hughes' solution for the if normalization challenge.

‎Archive/Examples/Kuratowski.lean‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,15 @@
1+
module
12
/-
23
Copyright (c) 2025 Jan Förster, Leon Müller, Luis Sand, and Junyan Xu. All rights reserved.
34
Released under Apache 2.0 license as described in the file LICENSE.
45
Authors: Jan Förster, Leon Müller, Luis Sand, Junyan Xu
56
-/
6-
import Mathlib.Topology.Instances.Irrational
7-
import Mathlib.Topology.Instances.Real.Lemmas
8-
import Archive.Kuratowski
7+
public import Mathlib.Topology.Instances.Irrational
8+
public import Mathlib.Topology.Instances.Real.Lemmas
9+
public import Archive.Kuratowski
10+
11+
12+
@[expose] public section
913

1014
/-!
1115
# Kuratowski's closure-complement theorem is sharp

‎Archive/Examples/MersennePrimes.lean‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,13 @@
1+
module
12
/-
23
Copyright (c) 2020 Kim Morrison. All rights reserved.
34
Released under Apache 2.0 license as described in the file LICENSE.
45
Authors: Kim Morrison
56
-/
6-
import Mathlib.NumberTheory.LucasLehmer
7+
public import Mathlib.NumberTheory.LucasLehmer
8+
9+
10+
@[expose] public section
711

812
/-!
913
# Explicit Mersenne primes

‎Archive/Examples/PropEncodable.lean‎

Lines changed: 10 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,14 @@
1+
module
12
/-
23
Copyright (c) 2019 Jeremy Avigad. All rights reserved.
34
Released under Apache 2.0 license as described in the file LICENSE.
45
Authors: Jeremy Avigad
56
-/
6-
import Mathlib.Data.W.Basic
7-
import Mathlib.Data.Fin.VecNotation
7+
public import Mathlib.Data.W.Basic
8+
public import Mathlib.Data.Fin.VecNotation
9+
10+
11+
@[expose] public section
812

913
/-!
1014
# W types
@@ -19,9 +23,6 @@ The strategy is to define a type of labels corresponding to the constructors.
1923
From the definition (using `sum`, `unit`, and an encodable type), Lean can infer
2024
that it is encodable. We then define a map from propositional formulas to the
2125
corresponding `Wfin` type, and show that map has a left inverse.
22-
23-
We mark the auxiliary constructions `private`, since their only purpose is to
24-
show encodability.
2526
-/
2627

2728

@@ -36,7 +37,7 @@ inductive PropForm (α : Type*)
3637

3738
namespace PropForm
3839

39-
private def Constructors (α : Type*) :=
40+
def Constructors (α : Type*) :=
4041
α ⊕ (Unit ⊕ (Unit ⊕ Unit))
4142

4243
local notation "cvar " a => Sum.inl a
@@ -48,7 +49,7 @@ local notation "cand" => Sum.inr (Sum.inr (Sum.inr Unit.unit))
4849
local notation "cor" => Sum.inr (Sum.inr (Sum.inl Unit.unit))
4950

5051
@[simp]
51-
private def arity (α : Type*) : Constructors α → Nat
52+
def arity (α : Type*) : Constructors α → Nat
5253
| cvar _ => 0
5354
| cnot => 1
5455
| cand => 2
@@ -61,13 +62,13 @@ instance : ∀ c : Unit ⊕ (Unit ⊕ Unit), NeZero (arity α (.inr c))
6162
| .inr (.inl ()) => ⟨two_ne_zero⟩
6263
| .inr (.inr ()) => ⟨two_ne_zero⟩
6364

64-
private def f : PropForm α → WType fun i => Fin (arity α i)
65+
def f : PropForm α → WType fun i => Fin (arity α i)
6566
| var a => ⟨cvar a, ![]⟩
6667
| not p => ⟨cnot, ![f p]⟩
6768
| and p q => ⟨cand, ![f p, f q]⟩
6869
| or p q => ⟨cor, ![f p, f q]⟩
6970

70-
private def finv : (WType fun i => Fin (arity α i)) → PropForm α
71+
def finv : (WType fun i => Fin (arity α i)) → PropForm α
7172
| ⟨cvar a, _⟩ => var a
7273
| ⟨cnot, fn⟩ => not (finv (fn 0))
7374
| ⟨cand, fn⟩ => and (finv (fn 0)) (finv (fn 1))

‎Archive/Hairer.lean‎

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,19 @@
1+
module
12
/-
23
Copyright (c) 2023 Floris van Doorn. All rights reserved.
34
Released under Apache 2.0 license as described in the file LICENSE.
45
Authors: Johan Commelin, Sébastien Gouëzel, Patrick Massot, Ruben Van de Velde, Floris van Doorn,
56
Junyan Xu
67
-/
7-
import Mathlib.Algebra.MvPolynomial.Funext
8-
import Mathlib.Analysis.Analytic.Polynomial
9-
import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
10-
import Mathlib.RingTheory.Algebraic.Integral
11-
import Mathlib.RingTheory.MvPolynomial.Basic
12-
import Mathlib.Topology.Algebra.MvPolynomial
8+
public import Mathlib.Algebra.MvPolynomial.Funext
9+
public import Mathlib.Analysis.Analytic.Polynomial
10+
public import Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
11+
public import Mathlib.RingTheory.Algebraic.Integral
12+
public import Mathlib.RingTheory.MvPolynomial.Basic
13+
public import Mathlib.Topology.Algebra.MvPolynomial
14+
15+
16+
@[expose] public section
1317

1418
/-!
1519
# Smooth functions whose integral calculates the values of polynomials

‎Archive/Imo/Imo1959Q1.lean‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,14 @@
1+
module
12
/-
23
Copyright (c) 2020 Kevin Lacker. All rights reserved.
34
Released under Apache 2.0 license as described in the file LICENSE.
45
Authors: Kevin Lacker
56
-/
6-
import Mathlib.Tactic.Ring
7-
import Mathlib.Data.Nat.Prime.Basic
7+
public import Mathlib.Tactic.Ring
8+
public import Mathlib.Data.Nat.Prime.Basic
9+
10+
11+
@[expose] public section
812

913
/-!
1014
# IMO 1959 Q1

0 commit comments

Comments
 (0)