Skip to content

chore: remove redundant imports in core #10750

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
+3 −1,921
Open

chore: remove redundant imports in core #10750

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
9c2fda2
chore: remove redundant imports in core
Kha Oct 12, 2025
d6cdea6
fix test
Kha Oct 12, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
The table of contents is too big for display.
Diff view
Diff view
  •  
  •  
  •  
1 change: 0 additions & 1 deletion src/Init/BinderNameHint.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ Authors: Joachim Breitner
module

prelude
public import Init.Prelude
public import Init.Tactics

public section
Expand Down
2 changes: 0 additions & 2 deletions src/Init/Control/EState.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,6 @@ Authors: Leonardo de Moura
module

prelude
public import Init.Control.State
public import Init.Control.Except
public import Init.Data.ToString.Basic

public section
Expand Down
1 change: 0 additions & 1 deletion src/Init/Control/Except.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,6 @@ module
prelude
public import Init.Control.Basic
public import Init.Control.Id
public import Init.Coe

@[expose] public section

Expand Down
2 changes: 0 additions & 2 deletions src/Init/Control/Lawful/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,6 @@ module

prelude
public import Init.Ext
public import Init.SimpLemmas
public import Init.Meta

public section

Expand Down
3 changes: 0 additions & 3 deletions src/Init/Control/Lawful/Instances.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,14 +7,11 @@ module

prelude
public import Init.Control.Lawful.Basic
public import Init.Control.Except
import all Init.Control.Except
public import Init.Control.Option
import all Init.Control.Option
public import Init.Control.State
import all Init.Control.State
public import Init.Control.StateRef
public import Init.Ext

public section

Expand Down
1 change: 0 additions & 1 deletion src/Init/Control/Lawful/Lemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ module

prelude
public import Init.Control.Lawful.Basic
public import Init.RCases
public import Init.ByCases

public section
Expand Down
4 changes: 0 additions & 4 deletions src/Init/Control/Lawful/MonadLift/Instances.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,17 +6,13 @@ Authors: Quang Dao, Paul Reichert
module

prelude
public import Init.Control.Option
import all Init.Control.Option
public import Init.Control.Except
import all Init.Control.Except
public import Init.Control.ExceptCps
import all Init.Control.ExceptCps
public import Init.Control.StateRef
import all Init.Control.StateRef
public import Init.Control.StateCps
import all Init.Control.StateCps
public import Init.Control.Id
import all Init.Control.Id
public import Init.Control.Lawful.MonadLift.Lemmas
public import Init.Control.Lawful.Instances
Expand Down
1 change: 0 additions & 1 deletion src/Init/Control/Option.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ module

prelude
public import Init.Data.Option.Basic
public import Init.Control.Basic
public import Init.Control.Except

public section
Expand Down
2 changes: 0 additions & 2 deletions src/Init/Control/Reader.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,6 @@ The Reader monad transformer for passing immutable State.
module

prelude
public import Init.Control.Basic
public import Init.Control.Id
public import Init.Control.Except

public section
Expand Down
2 changes: 0 additions & 2 deletions src/Init/Control/State.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,6 @@ The State monad transformer.
module

prelude
public import Init.Control.Basic
public import Init.Control.Id
public import Init.Control.Except

public section
Expand Down
1 change: 0 additions & 1 deletion src/Init/Core.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ notation, basic datatypes and type classes
module

prelude
public meta import Init.Prelude
public import Init.SizeOf

public section
Expand Down
1 change: 0 additions & 1 deletion src/Init/Data/AC.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ Authors: Dany Fabian
module

prelude
public import Init.Classical
public import Init.ByCases

@[expose] public section
Expand Down
3 changes: 0 additions & 3 deletions src/Init/Data/Array/Attach.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,7 @@ Authors: Joachim Breitner, Mario Carneiro
module

prelude
public import Init.Data.Array.Mem
public import Init.Data.Array.Lemmas
public import Init.Data.Array.Count
public import Init.Data.List.Attach
import all Init.Data.List.Attach

public section
Expand Down
4 changes: 0 additions & 4 deletions src/Init/Data/Array/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,6 @@ Authors: Leonardo de Moura
module

prelude
public import Init.WFTactics
public import Init.Data.Nat.Basic
public import Init.Data.Fin.Basic
public import Init.Data.UInt.BasicAux
public import Init.GetElem
public import Init.Data.List.ToArrayImpl
import all Init.Data.List.ToArrayImpl
Expand Down
2 changes: 0 additions & 2 deletions src/Init/Data/Array/BasicAux.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,8 @@ Authors: Leonardo de Moura
module

prelude
public import Init.Data.Array.Basic
import all Init.Data.Array.Basic
public import Init.Data.Nat.Linear
public import Init.NotationExtra

public section

Expand Down
2 changes: 0 additions & 2 deletions src/Init/Data/Array/BinSearch.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,7 @@ Authors: Leonardo de Moura
module

prelude
public import Init.Data.Array.Basic
public import Init.Data.Int.DivMod.Lemmas
public import Init.Omega

public section
universe u v
Expand Down
1 change: 0 additions & 1 deletion src/Init/Data/Array/Bootstrap.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@ module

prelude
public import Init.Data.List.TakeDrop
public import Init.Data.Array.Basic
import all Init.Data.Array.Basic

public section
Expand Down
1 change: 0 additions & 1 deletion src/Init/Data/Array/Count.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ Authors: Kim Morrison
module

prelude
public import Init.Data.Array.Basic
import all Init.Data.Array.Basic
public import Init.Data.Array.Lemmas
public import Init.Data.List.Nat.Count
Expand Down
2 changes: 0 additions & 2 deletions src/Init/Data/Array/DecidableEq.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,9 @@ Authors: Leonardo de Moura
module

prelude
public import Init.Data.Array.Basic
import all Init.Data.Array.Basic
public import Init.Data.BEq
public import Init.Data.List.Nat.BEq
public import Init.ByCases

public section

Expand Down
3 changes: 0 additions & 3 deletions src/Init/Data/Array/Erase.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,8 @@ Authors: Kim Morrison
module

prelude
public import Init.Data.Array.Basic
import all Init.Data.Array.Basic
public import Init.Data.Array.Lemmas
public import Init.Data.List.Nat.Erase
public import Init.Data.List.Nat.Basic

public section

Expand Down
1 change: 0 additions & 1 deletion src/Init/Data/Array/Extract.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ module

prelude
public import Init.Data.Array.Lemmas
public import Init.Data.List.Nat.TakeDrop

public section

Expand Down
1 change: 0 additions & 1 deletion src/Init/Data/Array/FinRange.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ Authors: François G. Dorais
module

prelude
public import Init.Data.List.FinRange
public import Init.Data.Array.OfFn

public section
Expand Down
3 changes: 0 additions & 3 deletions src/Init/Data/Array/Find.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,10 +7,7 @@ module

prelude
public import Init.Data.List.Nat.Find
public import Init.Data.Array.Basic
import all Init.Data.Array.Basic
public import Init.Data.Array.Lemmas
public import Init.Data.Array.Attach
public import Init.Data.Array.Range

public section
Expand Down
1 change: 0 additions & 1 deletion src/Init/Data/Array/InsertIdx.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ module

prelude
public import Init.Data.Array.Lemmas
public import Init.Data.List.Nat.InsertIdx

public section

Expand Down
7 changes: 0 additions & 7 deletions src/Init/Data/Array/Lemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,17 +6,10 @@ Authors: Mario Carneiro, Kim Morrison
module

prelude
public import Init.Data.Nat.Lemmas
public import Init.Data.List.Range
public import Init.Data.List.Nat.TakeDrop
public import Init.Data.List.Nat.Modify
public import Init.Data.List.Nat.Basic
public import Init.Data.List.Monadic
public import Init.Data.List.OfFn
public import Init.Data.Array.Mem
public import Init.Data.Array.DecidableEq
public import Init.Data.Range.Lemmas
public import Init.TacticsExtra
public import Init.Data.List.ToArray
import all Init.Data.List.Control
import all Init.Data.Array.Basic
Expand Down
3 changes: 0 additions & 3 deletions src/Init/Data/Array/Lex/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,9 +6,6 @@ Author: Kim Morrison
module

prelude
public import Init.Core
import Init.Data.Array.Basic
import Init.Data.Nat.Lemmas
public import Init.Data.Range.Polymorphic.Iterators
public import Init.Data.Range.Polymorphic.Nat
import Init.Data.Iterators.Consumers
Expand Down
2 changes: 0 additions & 2 deletions src/Init/Data/Array/Lex/Lemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,9 +10,7 @@ import all Init.Data.Array.Lex.Basic
public import Init.Data.Array.Lex.Basic
public import Init.Data.Array.Lemmas
public import Init.Data.List.Lex
import Init.Data.Range.Polymorphic.Lemmas
import Init.Data.Range.Polymorphic.NatLemmas
import Init.Data.Order.Lemmas

public section

Expand Down
3 changes: 0 additions & 3 deletions src/Init/Data/Array/MapIdx.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,7 @@ Authors: Mario Carneiro, Kim Morrison
module

prelude
public import Init.Data.Array.Basic
import all Init.Data.Array.Basic
public import Init.Data.Array.Lemmas
public import Init.Data.Array.Attach
public import Init.Data.Array.OfFn
public import Init.Data.List.MapIdx
import all Init.Data.List.MapIdx
Expand Down
2 changes: 0 additions & 2 deletions src/Init/Data/Array/Mem.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,8 +6,6 @@ Authors: Leonardo de Moura, Joachim Breitner
module

prelude
public import Init.Data.Array.Basic
public import Init.Data.Nat.Linear
public import Init.Data.List.BasicAux

public section
Expand Down
4 changes: 0 additions & 4 deletions src/Init/Data/Array/Monadic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,9 @@ Authors: Kim Morrison
module

prelude
public import Init.Data.List.Control
import all Init.Data.List.Control
public import Init.Data.Array.Basic
import all Init.Data.Array.Basic
public import Init.Data.Array.Lemmas
public import Init.Data.Array.Attach
public import Init.Data.List.Monadic

public section

Expand Down
3 changes: 0 additions & 3 deletions src/Init/Data/Array/OfFn.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,11 +6,8 @@ Authors: Kim Morrison
module

prelude
public import Init.Data.Array.Basic
import all Init.Data.Array.Basic
public import Init.Data.Array.Lemmas
public import Init.Data.Array.Monadic
public import Init.Data.List.OfFn
public import Init.Data.List.FinRange

public section
Expand Down
1 change: 0 additions & 1 deletion src/Init/Data/Array/Perm.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ module

prelude
public import Init.Data.List.Nat.Perm
public import Init.Data.Array.Basic
import all Init.Data.Array.Basic
public import Init.Data.Array.Lemmas

Expand Down
4 changes: 0 additions & 4 deletions src/Init/Data/Array/Range.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,14 +6,10 @@ Authors: Kim Morrison
module

prelude
public import Init.Data.Array.Lemmas
public import Init.Data.Array.Basic
import all Init.Data.Array.Basic
public import Init.Data.Array.OfFn
import all Init.Data.Array.OfFn
public import Init.Data.Array.MapIdx
public import Init.Data.Array.Zip
public import Init.Data.List.Nat.Range

public section

Expand Down
1 change: 0 additions & 1 deletion src/Init/Data/Array/Subarray.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ Authors: Leonardo de Moura
module

prelude
public import Init.GetElem
public import Init.Data.Array.Basic
import Init.Data.Array.GetLit
public import Init.Data.Slice.Basic
Expand Down
1 change: 0 additions & 1 deletion src/Init/Data/Array/Subarray/Split.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ Authors: David Thrane Christiansen
module

prelude
public import Init.Data.Array.Basic
public import Init.Data.Array.Subarray
import all Init.Data.Array.Subarray
public import Init.Omega
Expand Down
2 changes: 0 additions & 2 deletions src/Init/Data/Array/TakeDrop.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,8 @@ Authors: Markus Himmel
module

prelude
public import Init.Data.Array.Basic
import all Init.Data.Array.Basic
public import Init.Data.Array.Lemmas
public import Init.Data.List.Nat.TakeDrop

public section

Expand Down
2 changes: 0 additions & 2 deletions src/Init/Data/Array/Zip.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,8 @@ Authors: Kim Morrison
module

prelude
public import Init.Data.Array.Basic
import all Init.Data.Array.Basic
public import Init.Data.Array.TakeDrop
public import Init.Data.List.Zip

public section

Expand Down
8 changes: 0 additions & 8 deletions src/Init/Data/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,13 +6,5 @@ Authors: Leonardo de Moura
module

prelude
public import Init.Data.Nat.Basic
public import Init.Data.Fin.Basic
public import Init.Data.List.Basic
public import Init.Data.Char.Basic
public import Init.Data.String.Basic
public import Init.Data.Option.Basic
public import Init.Data.UInt
public import Init.Data.Repr
public import Init.Data.ToString.Basic
public import Init.Data.String.Extra
Loading
Loading