Index.lean

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

1import ZlibF.Proof.«inflate.c.window-platform»
2import ZlibF.Proof.«public-deflate-init»
3import ZlibF.Proof.«gzlib.c.open»
4import ZlibF.Proof.«gzread.c.close»
5import ZlibF.Proof.«deflate.c.prime»
6import ZlibF.Proof.ByteAddress
7import ZlibF.Proof.«crc32.c.views»
8import ZlibF.Proof.«public-crc-updates»
9import ZlibF.Proof.Api.HeaderRoundtrip
10import ZlibF.Proof.Api.DictionaryRoundtrip
11import ZlibF.Proof.Api.GzipRoundtrip
12import ZlibF.Proof.Api.Roundtrip
13import ZlibF.Proof.Api.DeflateFlush
14import ZlibF.Proof.Api.GzRoundtrip
15import ZlibF.Proof.Api.CompressRoundtrip
16import ZlibF.Proof.Api.DeflateBounds
17import ZlibF.Proof.«public-inflate-setdict»
18import ZlibF.Proof.«trees.c.send-support»
19
20import ZlibF.Proof.«inffast.c.platform»
21import ZlibF.Proof.«inflate.c.platform»
22import ZlibF.Proof.«inftrees.c.content»
23import ZlibF.Proof.«inftrees.c.read-extent»
24
25import ZlibF.Proof.«inflate.c.lookup-codes»
26
27/-!
28Proof-only import point. Add new proof modules here without changing the locked root.
29Every imported declaration still passes the kernel, semantic-lock and assumption gates.
30-/