ZlibF.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Runtime.Space
2import ZlibF.Runtime.Schema
3import ZlibF.Runtime.Monad
4import ZlibF.Runtime.Ptr
5import ZlibF.Runtime.Alloc
6import ZlibF.Runtime.Libc
7import ZlibF.Runtime.LibcTables
8import ZlibF.Runtime.Tables
9import ZlibF.Zlib.«adler32.c»
10import ZlibF.Proof.«adler32.c»
11import ZlibF.Zlib.«zutil.c»
12import ZlibF.Proof.«zutil.c»
13import ZlibF.Proof.«crc32.c»
14import ZlibF.Proof.«inftrees.c.math»
15import ZlibF.Proof.«inftrees.c.base»
16import ZlibF.Proof.«inftrees.c.geom»
17import ZlibF.Proof.«inftrees.c.step»
18import ZlibF.Proof.«inftrees.c.spec»
19import ZlibF.Proof.«inftrees.c.link»
20import ZlibF.Proof.«inftrees.c.canon»
21import ZlibF.Proof.«inftrees.c.canonbridge»
22import ZlibF.Proof.«inftrees.c.main»
23import ZlibF.Proof.«inftrees.c»
24import ZlibF.Spec.Format
25import ZlibF.Zlib.«crc32.h»
26import ZlibF.Zlib.«crc32.c»
27import ZlibF.Zlib.«inffixed.h»
28import ZlibF.Zlib.«inftrees.c»
29import ZlibF.Zlib.«inffast.c»
30import ZlibF.Zlib.«zutil.c»
31import ZlibF.Zlib.«trees.c»
32import ZlibF.Zlib.«deflate_base.c»
33import ZlibF.Zlib.«deflate_strategies.c»
34import ZlibF.Zlib.«deflate.c»
35import ZlibF.Zlib.«compress.c»
36import ZlibF.Zlib.gzfs
37import ZlibF.Zlib.«gzguts.h»
38import ZlibF.Zlib.«gzlib.c»
39import ZlibF.Zlib.«gzread.c»
40import ZlibF.Zlib.«gzwrite.c»
41import ZlibF.Zlib.«gzclose.c»
42import ZlibF.Zlib.«uncompr.c»
43import ZlibF.Proof.Format.Api
44import ZlibF.Proof.«inflate.c.base»
45import ZlibF.Proof.«inflate.c.reset»
46import ZlibF.Proof.«inflate.c.init»
47import ZlibF.Proof.«inflate.c.end»
48import ZlibF.Proof.«inflate.c.start»
49import ZlibF.Proof.«inflate.c.misc»
50import ZlibF.Proof.«inflate.c.misc2»
51import ZlibF.Proof.«inflate.c.window»
52import ZlibF.Proof.«inflate.c.witness»
53import ZlibF.Proof.«inflate.c.main.bits»
54import ZlibF.Proof.«inflate.c.main.xloop»
55import ZlibF.Proof.«inflate.c.main.macros»
56import ZlibF.Proof.«inflate.c.main.simple»
57import ZlibF.Proof.«inflate.c.main.common»
58import ZlibF.Proof.«inflate.c.main.type»
59import ZlibF.Proof.«inflate.c.main.stored»
60import ZlibF.Proof.«inflate.c.main.stored2»
61import ZlibF.Proof.«trees.c.heap.base»
62import ZlibF.Proof.«trees.c.heap.ord»
63import ZlibF.Proof.«trees.c.heap.pq»
64import ZlibF.Proof.«trees.c.heap.pqrun»
65import ZlibF.Proof.«trees.c.heap.gbmath»
66import ZlibF.Proof.«trees.c.heap.gbtree»
67import ZlibF.Proof.«trees.c.heap.gbdef»
68import ZlibF.Proof.«infback.c.init»
69import ZlibF.Proof.«infback.c.end»
70import ZlibF.Proof.«infback.c.callbacks»
71import ZlibF.Proof.«infback.c.back»
72import ZlibF.Proof.«inftrees.c.fixed»
73import ZlibF.Proof.«inffast.c.len»
74import ZlibF.Proof.«deflate.c.base»
75import ZlibF.Proof.«trees.c.heap.gbclk»
76import ZlibF.Proof.«trees.c.heap.gbp1»
77import ZlibF.Proof.«inflate.c.uw»
78import ZlibF.Proof.«trees.c.inv»
79import ZlibF.Proof.«trees.c.bits»
80import ZlibF.Proof.«trees.c.reverse»
81import ZlibF.Proof.«trees.c.codes»
82import ZlibF.Proof.«trees.c.build.leaves»
83import ZlibF.Proof.«trees.c.build.order»
84import ZlibF.Proof.«trees.c.build.tail»
85import ZlibF.Proof.«trees.c.arrays»
86import ZlibF.Proof.«trees.c.block»
87import ZlibF.Proof.«trees.c.emit»
88import ZlibF.Proof.«trees.c.align»
89import ZlibF.Proof.«inftrees.c.cover.tile»
90import ZlibF.Proof.«inftrees.c.cover.root»
91import ZlibF.Proof.«inftrees.c.cover.group»
92import ZlibF.Proof.«inftrees.c.cover.fn»
93import ZlibF.Proof.«inftrees.c.cover.leaf»
94import ZlibF.Proof.«inftrees.c.cover.stmt»
95import ZlibF.Proof.«infback.c.macros»
96import ZlibF.Proof.«infback.c.room»
97import ZlibF.Proof.«infback.c.inv»
98import ZlibF.Proof.«deflate.c.life.check»
99import ZlibF.Proof.«deflate.c.life.bound»
100import ZlibF.Proof.«deflate.c.life.end»
101import ZlibF.Proof.«deflate.c.life.reset»
102import ZlibF.Proof.«inflate.c.main.check0»
103import ZlibF.Proof.«inflate.c.main.check»
104import ZlibF.Proof.«inflate.c.main.table»
105import ZlibF.Proof.«inflate.c.main.table2»
106import ZlibF.Proof.«inflate.c.main.table3»
107import ZlibF.Proof.«inflate.c.main.table4»
108import ZlibF.Proof.«inflate.c.main.table5»
109import ZlibF.Proof.«inflate.c.main.table6»
110import ZlibF.Proof.«trees.c.tally»
111import ZlibF.Proof.«gzlib.c.base»
112import ZlibF.Proof.«gzlib.c.error»
113import ZlibF.Proof.«gzlib.c.simple»
114import ZlibF.Proof.«gzlib.c.rewind»
115import ZlibF.Proof.«gzlib.c.seek»
116import ZlibF.Proof.«gzclose.c»
117import ZlibF.Proof.«inflate.c.hdr»
118import ZlibF.Proof.«inflate.c.sync»
119import ZlibF.Proof.«inflate.c.sync2»
120import ZlibF.Proof.«deflate.c.engine.hash»
121import ZlibF.Proof.«deflate.c.engine.chains»
122import ZlibF.Proof.«deflate.c.engine.window»
123import ZlibF.Proof.«deflate.c.engine.match»
124import ZlibF.Proof.«deflate.c.engine.macros»
125import ZlibF.Proof.«deflate.c.engine.slide»
126import ZlibF.Proof.«inflate.c.ring»
127import ZlibF.Proof.«trees.c.heap.gbfix»
128import ZlibF.Proof.«trees.c.heap.gbre»
129import ZlibF.Proof.«trees.c.heap.gbsym»
130import ZlibF.Proof.«trees.c.heap.gbtop»
131import ZlibF.Proof.«inflate.c.dict»
132import ZlibF.Proof.«trees.c.runs»
133import ZlibF.Proof.«deflate.c.engine.loops»
134import ZlibF.Proof.«deflate.c.engine.lmcond»
135import ZlibF.Proof.«deflate.c.engine.lminner»
136import ZlibF.Proof.«deflate.c.engine.lmbody»
137import ZlibF.Proof.«deflate.c.engine.lmmain»
138import ZlibF.Proof.«deflate.c.engine.readbuf»
139import ZlibF.Proof.«infback.c.pure»
140import ZlibF.Proof.«infback.c.wf»
141import ZlibF.Proof.«infback.c.pull»
142import ZlibF.Proof.«infback.c.stored»
143import ZlibF.Proof.«inflate.c.sync3»
144import ZlibF.Proof.«inflate.c.sync4»
145import ZlibF.Proof.«deflate.c.life.getdict»
146import ZlibF.Spec.Api.Concrete
147import ZlibF.Spec.Api
148import ZlibF.Proof.gzfs
149import ZlibF.Proof.Api.Compress
150import ZlibF.Proof.Api.Deflate
151import ZlibF.Proof.Api.Concrete
152import ZlibF.Proof.Api.CompressBoundary
153import ZlibF.Proof.Api.CompressFailure
154import ZlibF.Proof.Api.Inflate
155
156import ZlibF.Spec.Public.Calls
157import ZlibF.Spec.Public.Queries
158import ZlibF.Spec.Public.Checksums
159import ZlibF.Spec.Public.StreamQueries
160import ZlibF.Spec.Public.Utilities
161import ZlibF.Spec.Public.Initialisation
162import ZlibF.Spec.Public.Lifecycle
163import ZlibF.Spec.Public.History
164import ZlibF.Spec.Public.Streams
165import ZlibF.Spec.Public.Copy
166import ZlibF.Spec.Public.GzState
167import ZlibF.Spec.Public.GzControl
168import ZlibF.Spec.Public.GzOpen
169import ZlibF.Spec.Public.GzRead
170import ZlibF.Spec.Public.GzWrite
171import ZlibF.Spec.Public.GzClose
172import ZlibF.Spec.Public.Back
173import ZlibF.Spec.Public.Domains
174import ZlibF.Spec.Public.GzTrace
175import ZlibF.Spec.Public.Sequences
176import ZlibF.Proof.«public-gzeof»
177import ZlibF.Proof.«public-gzbuffer»
178import ZlibF.Proof.«inffast.c.origin»
179import ZlibF.Proof.«inffast.c.call-origin»
180import ZlibF.Proof.«inffast.c.distance-semantics»
181import ZlibF.Proof.«inffast.c.distance-result»
182import ZlibF.Proof.«inffast.c.length-semantics»
183import ZlibF.Proof.«inffast.c.length-trace»
184import ZlibF.Proof.«inffast.c.body-token»
185import ZlibF.Proof.Format.Token
186
187import ZlibF.Proof.Api.HeapCleanup
188import ZlibF.Proof.Api.QueryLayout
189import ZlibF.Proof.«gzlib.c.public-clearerr»
190import ZlibF.Proof.Index
191import ZlibF.Proof.«public-zlib-compile-flags»
192import ZlibF.Proof.«public-zlib-version»
193import ZlibF.Proof.«public-zerror»
194import ZlibF.Proof.«public-compress-bound»
195import ZlibF.Proof.«public-get-crc-table»
196import ZlibF.Proof.«public-gz-offset»
197import ZlibF.Proof.«public-gz-error»
198import ZlibF.Proof.«public-inflate-small-queries»
199import ZlibF.Proof.«public-deflate-small-queries»
200import ZlibF.Proof.«public-inflate-mark»
201import ZlibF.Proof.«public-inflate-prime»
202import ZlibF.Proof.«public-gz-rewind»
203import ZlibF.Proof.«public-inflate-header»
204import ZlibF.Proof.«public-inflate-reset-keep»
205import ZlibF.Proof.«public-inflate-reset»
206import ZlibF.Proof.«public-inflate-reset2»
207import ZlibF.Proof.«public-inflate-end»
208import ZlibF.Proof.«public-infback-end»
209import ZlibF.Proof.«public-deflate-end»
210import ZlibF.Proof.«public-deflate-getdict»
211import ZlibF.Proof.«public-inflate-getdict»
212import ZlibF.Proof.«public-deflate-reset-keep»
213import ZlibF.Proof.«public-deflate-reset»
214import ZlibF.Proof.«public-inflate-init»
215import ZlibF.Proof.«public-infback-init»
216import ZlibF.Proof.«public-adler-combine»
217import ZlibF.Proof.«public-crc-combine»
218import ZlibF.Proof.«public-adler-update»