Skip to content

Commit 58d757d

Browse files
committed
shuffle imports a little bit more
1 parent 83ecf37 commit 58d757d

File tree

4 files changed

+11
-35
lines changed

4 files changed

+11
-35
lines changed

ArkLib.lean

Lines changed: 11 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -5,33 +5,30 @@ import ArkLib.CommitmentScheme.MerkleTree
55
import ArkLib.CommitmentScheme.SimpleRO
66
import ArkLib.CommitmentScheme.Tensor
77
import ArkLib.CommitmentScheme.Trivial
8-
import ArkLib.Data.CodingTheory.Basic
9-
import ArkLib.Data.CodingTheory.JohnsonBound
10-
import ArkLib.Data.CodingTheory.ProximityGap
11-
import ArkLib.Data.CodingTheory.ReedMuller
12-
import ArkLib.Data.CodingTheory.ReedSolomon
138
import ArkLib.Data.Classes.DCast
149
import ArkLib.Data.Classes.HasSize
1510
import ArkLib.Data.Classes.Initialize
1611
import ArkLib.Data.Classes.Serde
1712
import ArkLib.Data.Classes.Zeroize
18-
import ArkLib.Data.CodingTheory
1913
import ArkLib.Data.CodingTheory.Basic
20-
import ArkLib.Data.CodingTheory.BerlekampWelch
21-
import ArkLib.Data.CodingTheory.BerlekampWelch.BerlekampWelch
22-
import ArkLib.Data.CodingTheory.BerlekampWelch.Condition
23-
import ArkLib.Data.CodingTheory.BerlekampWelch.ElocPoly
24-
import ArkLib.Data.CodingTheory.BerlekampWelch.Existence
25-
import ArkLib.Data.CodingTheory.BerlekampWelch.Sorries
26-
import ArkLib.Data.CodingTheory.BerlekampWelch.ToMathlib
27-
import ArkLib.Data.CodingTheory.DivergenceOfSets
2814
import ArkLib.Data.CodingTheory.InterleavedCode
2915
import ArkLib.Data.CodingTheory.ListDecodability
3016
import ArkLib.Data.CodingTheory.PolishchukSpielman
3117
import ArkLib.Data.CodingTheory.Prelims
3218
import ArkLib.Data.CodingTheory.ProximityGap
3319
import ArkLib.Data.CodingTheory.ReedMuller
3420
import ArkLib.Data.CodingTheory.ReedSolomon
21+
import ArkLib.Data.CodingTheory.BerlekampWelch.BerlekampWelch
22+
import ArkLib.Data.CodingTheory.BerlekampWelch.Condition
23+
import ArkLib.Data.CodingTheory.BerlekampWelch.ElocPoly
24+
import ArkLib.Data.CodingTheory.BerlekampWelch.Existence
25+
import ArkLib.Data.CodingTheory.BerlekampWelch.Sorries
26+
import ArkLib.Data.CodingTheory.BerlekampWelch.ToMathlib
27+
import ArkLib.Data.CodingTheory.DivergenceOfSets
28+
import ArkLib.Data.CodingTheory.JohnsonBound.Basic
29+
import ArkLib.Data.CodingTheory.JohnsonBound.Choose2
30+
import ArkLib.Data.CodingTheory.JohnsonBound.Expectations
31+
import ArkLib.Data.CodingTheory.JohnsonBound.Lemmas
3532
import ArkLib.Data.EllipticCurve.BN254
3633
import ArkLib.Data.FieldTheory.BinaryField.AdditiveNTT.NovelPolynomialBasis
3734
import ArkLib.Data.FieldTheory.BinaryField.AdditiveNTT.Prelude

ArkLib/Data/CodingTheory.lean

Lines changed: 0 additions & 11 deletions
This file was deleted.

ArkLib/Data/CodingTheory/BerlekampWelch.lean

Lines changed: 0 additions & 6 deletions
This file was deleted.

ArkLib/Data/CodingTheory/JohnsonBound.lean

Lines changed: 0 additions & 4 deletions
This file was deleted.

0 commit comments

Comments
 (0)