Repository navigation
Expand file tree
/
Copy pathPrimeGapsCert.lean
More file actions
179 lines (178 loc) · 9.72 KB
/
Copy pathPrimeGapsCert.lean
File metadata and controls
179 lines (178 loc) · 9.72 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
module -- shake: keep-all --deprecated_module: ignore
public import PrimeGapsCert.Gap246.Certificate.Defs
public import PrimeGapsCert.Gap246.Certificate.Fast
public import PrimeGapsCert.Gap246.Certificate.MomentSound
public import PrimeGapsCert.Gap246.Data.Defs
public import PrimeGapsCert.Gap246.Data.Generated
public import PrimeGapsCert.Gap246.Data.Packed
public import PrimeGapsCert.Gap246.Data.Sound
public import PrimeGapsCert.Gap246.Emit.AllCommands
public import PrimeGapsCert.Gap246.Emit.Commands
public import PrimeGapsCert.Gap246.Emit.Gen
public import PrimeGapsCert.Gap246.Emit.LevelCommands
public import PrimeGapsCert.Gap246.Emit.LevelDataCommands
public import PrimeGapsCert.Gap246.Emit.ResultCommands
public import PrimeGapsCert.Gap246.Emit.SourceGen
public import PrimeGapsCert.Gap246.Emit.State
public import PrimeGapsCert.Gap246.Kernel.Core
public import PrimeGapsCert.Gap246.Kernel.Extra
public import PrimeGapsCert.Gap246.Kernel.Folds
public import PrimeGapsCert.Gap246.Kernel.LHS
public import PrimeGapsCert.Gap246.Kernel.LHSScalar
public import PrimeGapsCert.Gap246.Kernel.MomentBound
public import PrimeGapsCert.Gap246.Kernel.Moments
public import PrimeGapsCert.Gap246.Kernel.RHS
public import PrimeGapsCert.Gap246.Kernel.RHSFormula
public import PrimeGapsCert.Gap246.LHS.Assembly
public import PrimeGapsCert.Gap246.LHS.Assembly.RowSum
public import PrimeGapsCert.Gap246.LHS.Assembly.RowsComplete
public import PrimeGapsCert.Gap246.LHS.Assembly.StoredRowSum
public import PrimeGapsCert.Gap246.LHS.Assembly.Transform
public import PrimeGapsCert.Gap246.LHS.Checks
public import PrimeGapsCert.Gap246.LHS.Checks.Index
public import PrimeGapsCert.Gap246.LHS.Checks.Slice00
public import PrimeGapsCert.Gap246.LHS.Checks.Slice01
public import PrimeGapsCert.Gap246.LHS.Checks.Slice02
public import PrimeGapsCert.Gap246.LHS.Checks.Slice03
public import PrimeGapsCert.Gap246.LHS.Checks.Slice04
public import PrimeGapsCert.Gap246.LHS.Checks.Slice05
public import PrimeGapsCert.Gap246.LHS.Checks.Slice06
public import PrimeGapsCert.Gap246.LHS.Checks.Slice07
public import PrimeGapsCert.Gap246.LHS.Checks.Slice08
public import PrimeGapsCert.Gap246.LHS.Checks.Slice09
public import PrimeGapsCert.Gap246.LHS.ConcreteSound.Contraction
public import PrimeGapsCert.Gap246.LHS.ConcreteSound.Rows
public import PrimeGapsCert.Gap246.LHS.ConcreteSound.Scalar
public import PrimeGapsCert.Gap246.LHS.ConcreteSound.Transform
public import PrimeGapsCert.Gap246.LHS.Data
public import PrimeGapsCert.Gap246.LHS.Data.Generated
public import PrimeGapsCert.Gap246.LHS.Data.Index
public import PrimeGapsCert.Gap246.LHS.Data.Rows
public import PrimeGapsCert.Gap246.LHS.Data.Scalars
public import PrimeGapsCert.Gap246.LHS.Data.Transform
public import PrimeGapsCert.Gap246.LHS.Defs
public import PrimeGapsCert.Gap246.LHS.HighLevel
public import PrimeGapsCert.Gap246.LHS.ScalarDefs
public import PrimeGapsCert.Gap246.Moments.Assembly
public import PrimeGapsCert.Gap246.Moments.BoundAssembly
public import PrimeGapsCert.Gap246.Moments.BoundSound
public import PrimeGapsCert.Gap246.Moments.CheckSound
public import PrimeGapsCert.Gap246.Moments.Checks
public import PrimeGapsCert.Gap246.Moments.Checks.Ready
public import PrimeGapsCert.Gap246.Moments.Checks.Result
public import PrimeGapsCert.Gap246.Moments.Checks.ResultWorkers.Worker01
public import PrimeGapsCert.Gap246.Moments.Checks.ResultWorkers.Worker02
public import PrimeGapsCert.Gap246.Moments.Checks.ResultWorkers.Worker03
public import PrimeGapsCert.Gap246.Moments.Checks.ResultWorkers.Worker04
public import PrimeGapsCert.Gap246.Moments.Checks.ResultWorkers.Worker05
public import PrimeGapsCert.Gap246.Moments.Checks.ResultWorkers.Worker06
public import PrimeGapsCert.Gap246.Moments.Checks.ResultWorkers.Worker07
public import PrimeGapsCert.Gap246.Moments.Checks.ResultWorkers.Worker08
public import PrimeGapsCert.Gap246.Moments.Checks.ResultWorkers.Worker09
public import PrimeGapsCert.Gap246.Moments.Checks.Workers.Worker01
public import PrimeGapsCert.Gap246.Moments.Checks.Workers.Worker02
public import PrimeGapsCert.Gap246.Moments.Checks.Workers.Worker03
public import PrimeGapsCert.Gap246.Moments.Checks.Workers.Worker04
public import PrimeGapsCert.Gap246.Moments.Checks.Workers.Worker05
public import PrimeGapsCert.Gap246.Moments.Checks.Workers.Worker06
public import PrimeGapsCert.Gap246.Moments.Checks.Workers.Worker07
public import PrimeGapsCert.Gap246.Moments.Checks.Workers.Worker08
public import PrimeGapsCert.Gap246.Moments.Checks.WorkersReady
public import PrimeGapsCert.Gap246.Moments.CoeffCheck
public import PrimeGapsCert.Gap246.Moments.Direct.DataCheckSound
public import PrimeGapsCert.Gap246.Moments.Direct.DecodeSound
public import PrimeGapsCert.Gap246.Moments.Direct.LadderSound
public import PrimeGapsCert.Gap246.Moments.Direct.Spec
public import PrimeGapsCert.Gap246.Moments.Direct.StepEntryH
public import PrimeGapsCert.Gap246.Moments.Gather
public import PrimeGapsCert.Gap246.Moments.Generated
public import PrimeGapsCert.Gap246.Moments.LadderSound
public import PrimeGapsCert.Gap246.Moments.LevelConcreteSound
public import PrimeGapsCert.Gap246.Moments.LevelDefs
public import PrimeGapsCert.Gap246.Moments.LevelGather
public import PrimeGapsCert.Gap246.Moments.LevelReady
public import PrimeGapsCert.Gap246.Moments.NilEntrySound
public import PrimeGapsCert.Gap246.Moments.NilSupport
public import PrimeGapsCert.Gap246.Moments.PairDefs
public import PrimeGapsCert.Gap246.Moments.ResultSound
public import PrimeGapsCert.Gap246.Moments.ScanLemmas
public import PrimeGapsCert.Gap246.Moments.Spec
public import PrimeGapsCert.Gap246.Moments.TableSound
public import PrimeGapsCert.Gap246.RHS.Assembly
public import PrimeGapsCert.Gap246.RHS.Assembly.FeatureComplete
public import PrimeGapsCert.Gap246.RHS.Assembly.KeyChecks
public import PrimeGapsCert.Gap246.RHS.Assembly.RadialChecks
public import PrimeGapsCert.Gap246.RHS.Assembly.RowSum
public import PrimeGapsCert.Gap246.RHS.Assembly.RowsComplete
public import PrimeGapsCert.Gap246.RHS.Assembly.StoredRowSum
public import PrimeGapsCert.Gap246.RHS.Assembly.Transform
public import PrimeGapsCert.Gap246.RHS.Checks
public import PrimeGapsCert.Gap246.RHS.Checks.Index
public import PrimeGapsCert.Gap246.RHS.Checks.Slice00
public import PrimeGapsCert.Gap246.RHS.Checks.Slice01
public import PrimeGapsCert.Gap246.RHS.Checks.Slice02
public import PrimeGapsCert.Gap246.RHS.Checks.Slice03
public import PrimeGapsCert.Gap246.RHS.Checks.Slice04
public import PrimeGapsCert.Gap246.RHS.Checks.Slice05
public import PrimeGapsCert.Gap246.RHS.Checks.Slice06
public import PrimeGapsCert.Gap246.RHS.Checks.Slice07
public import PrimeGapsCert.Gap246.RHS.Checks.Slice08
public import PrimeGapsCert.Gap246.RHS.Checks.Slice09
public import PrimeGapsCert.Gap246.RHS.Checks.Weight
public import PrimeGapsCert.Gap246.RHS.Checks.Weight.Balance
public import PrimeGapsCert.Gap246.RHS.Checks.Weight.Combined
public import PrimeGapsCert.Gap246.RHS.Checks.Weight.Expected01
public import PrimeGapsCert.Gap246.RHS.Checks.Weight.Expected02
public import PrimeGapsCert.Gap246.RHS.Checks.Weight.Expected03
public import PrimeGapsCert.Gap246.RHS.Checks.Weight.Expected04
public import PrimeGapsCert.Gap246.RHS.Checks.Weight.Source01
public import PrimeGapsCert.Gap246.RHS.Checks.Weight.Source02
public import PrimeGapsCert.Gap246.RHS.Checks.Weight.Source03
public import PrimeGapsCert.Gap246.RHS.Checks.Weight.Source04
public import PrimeGapsCert.Gap246.RHS.Checks.Weight.Source05
public import PrimeGapsCert.Gap246.RHS.Checks.Weight.Source06
public import PrimeGapsCert.Gap246.RHS.ConcreteSound
public import PrimeGapsCert.Gap246.RHS.ConcreteSound.Contraction
public import PrimeGapsCert.Gap246.RHS.ConcreteSound.Rows
public import PrimeGapsCert.Gap246.RHS.ConcreteSound.Transform
public import PrimeGapsCert.Gap246.RHS.ConcreteSound.Transform.Basic
public import PrimeGapsCert.Gap246.RHS.ConcreteSound.Transform.Checked
public import PrimeGapsCert.Gap246.RHS.ConcreteSound.Transform.Direct
public import PrimeGapsCert.Gap246.RHS.Data
public import PrimeGapsCert.Gap246.RHS.Data.ExpectedWeightCheckpoints
public import PrimeGapsCert.Gap246.RHS.Data.Generated
public import PrimeGapsCert.Gap246.RHS.Data.Index
public import PrimeGapsCert.Gap246.RHS.Data.Location
public import PrimeGapsCert.Gap246.RHS.Data.Radial
public import PrimeGapsCert.Gap246.RHS.Data.Rows
public import PrimeGapsCert.Gap246.RHS.Data.SourceWeightCheckpoints
public import PrimeGapsCert.Gap246.RHS.Data.Transform
public import PrimeGapsCert.Gap246.RHS.Defs
public import PrimeGapsCert.Gap246.RHS.FeatureSound
public import PrimeGapsCert.Gap246.RHS.HighLevel
public import PrimeGapsCert.Gap246.RHS.WeightBridge
public import PrimeGapsCert.Gap246.RHS.WeightDefs
public import PrimeGapsCert.Gap246.Sparse.AccessorBridge
public import PrimeGapsCert.Gap246.Sparse.DataCommands
public import PrimeGapsCert.Gap246.Sparse.Gen
public import PrimeGapsCert.Gap246.Sparse.LhsCommands
public import PrimeGapsCert.Gap246.Sparse.LhsSound
public import PrimeGapsCert.Gap246.Sparse.RhsCommands
public import PrimeGapsCert.Gap246.Sparse.RhsContractionSound
public import PrimeGapsCert.Gap246.Sparse.RhsFeatureSound
public import PrimeGapsCert.Gap246.Sparse.RhsIndexSound
public import PrimeGapsCert.Gap246.Sparse.RhsRowSound
public import PrimeGapsCert.Gap246.Sparse.RhsTransformSound
public import PrimeGapsCert.Gap246.Sparse.SignedSound
public import PrimeGapsCert.Gap246.Sparse.WeightBase
public import PrimeGapsCert.Gap246.Sparse.WeightCore
public import PrimeGapsCert.Gap246.Sparse.WeightDigits
public import PrimeGapsCert.Gap246.Sparse.WeightExpected
public import PrimeGapsCert.Gap246.Sparse.WeightSound
public import PrimeGapsCert.Gap246.Sparse.WeightSource
public import PrimeGapsCert.Gap246.Sums
public import PrimeGapsCert.Gap246.Witness
public import PrimeGapsCert.Gap600.Witness
public import PrimeGapsCert.Meta.Basic
public import PrimeGapsCert.Meta.Batched
public import PrimeGapsCert.Meta.Gap600