Skip to content

Commit c07c998

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

4 files changed

Lines changed: 4 additions & 28 deletions

File tree

ArkLib.lean

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -5,19 +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
2114
import ArkLib.Data.CodingTheory.BerlekampWelch.BerlekampWelch
2215
import ArkLib.Data.CodingTheory.BerlekampWelch.Condition
2316
import ArkLib.Data.CodingTheory.BerlekampWelch.ElocPoly
@@ -26,6 +19,10 @@ import ArkLib.Data.CodingTheory.BerlekampWelch.Sorries
2619
import ArkLib.Data.CodingTheory.BerlekampWelch.ToMathlib
2720
import ArkLib.Data.CodingTheory.DivergenceOfSets
2821
import ArkLib.Data.CodingTheory.InterleavedCode
22+
import ArkLib.Data.CodingTheory.JohnsonBound.Basic
23+
import ArkLib.Data.CodingTheory.JohnsonBound.Choose2
24+
import ArkLib.Data.CodingTheory.JohnsonBound.Expectations
25+
import ArkLib.Data.CodingTheory.JohnsonBound.Lemmas
2926
import ArkLib.Data.CodingTheory.ListDecodability
3027
import ArkLib.Data.CodingTheory.PolishchukSpielman
3128
import ArkLib.Data.CodingTheory.Prelims

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)