Skip to content

Commit 1ec9dbd

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

4 files changed

Lines changed: 10 additions & 34 deletions

File tree

ArkLib.lean

Lines changed: 10 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -5,25 +5,12 @@ 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
2714
import ArkLib.Data.CodingTheory.DivergenceOfSets
2815
import ArkLib.Data.CodingTheory.InterleavedCode
2916
import ArkLib.Data.CodingTheory.ListDecodability
@@ -32,6 +19,16 @@ import ArkLib.Data.CodingTheory.Prelims
3219
import ArkLib.Data.CodingTheory.ProximityGap
3320
import ArkLib.Data.CodingTheory.ReedMuller
3421
import ArkLib.Data.CodingTheory.ReedSolomon
22+
import ArkLib.Data.CodingTheory.BerlekampWelch.BerlekampWelch
23+
import ArkLib.Data.CodingTheory.BerlekampWelch.Condition
24+
import ArkLib.Data.CodingTheory.BerlekampWelch.ElocPoly
25+
import ArkLib.Data.CodingTheory.BerlekampWelch.Existence
26+
import ArkLib.Data.CodingTheory.BerlekampWelch.Sorries
27+
import ArkLib.Data.CodingTheory.BerlekampWelch.ToMathlib
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)