参考文档 / ZLIB × LEAN
Lean 源码与证明正文
按用途查找 Lean 模块：实现证明、函数规格、数学推导、运行时模型或 C 翻译。可以按模块路径或声明名搜索。
DeflateBlIndex.leanZlibF/Math/DeflateBlIndex.lean数学推导↗DeflateCodes.leanZlibF/Math/DeflateCodes.lean数学推导↗DeflateForest.leanZlibF/Math/DeflateForest.lean数学推导↗DeflateHeap.leanZlibF/Math/DeflateHeap.lean数学推导↗DeflateHeapRemove.leanZlibF/Math/DeflateHeapRemove.lean数学推导↗DeflateKraft.leanZlibF/Math/DeflateKraft.lean数学推导↗DeflateRunSupport.leanZlibF/Math/DeflateRunSupport.lean数学推导↗DeflateTreeForce.leanZlibF/Math/DeflateTreeForce.lean数学推导↗DeflateTreeScan.leanZlibF/Math/DeflateTreeScan.lean数学推导↗InflateFastMatchHistory.leanZlibF/Math/InflateFastMatchHistory.lean数学推导↗InflatePrefixes.leanZlibF/Math/InflatePrefixes.lean数学推导↗InflateTableCoverage.leanZlibF/Math/InflateTableCoverage.lean数学推导↗InflateTableGeometry.leanZlibF/Math/InflateTableGeometry.lean数学推导↗LZ77Copy.leanZlibF/Math/LZ77Copy.lean数学推导↗LZ77CopySpec.leanZlibF/Math/LZ77CopySpec.lean数学推导↗LZ77History.leanZlibF/Math/LZ77History.lean数学推导↗LZ77HistorySpec.leanZlibF/Math/LZ77HistorySpec.lean数学推导↗Compress.leanZlibF/Proof/Api/Compress.lean实现证明↗CompressBoundary.leanZlibF/Proof/Api/CompressBoundary.lean实现证明↗CompressFailure.leanZlibF/Proof/Api/CompressFailure.lean实现证明↗CompressRoundtrip.leanZlibF/Proof/Api/CompressRoundtrip.lean实现证明↗Concrete.leanZlibF/Proof/Api/Concrete.lean实现证明↗Deflate.leanZlibF/Proof/Api/Deflate.lean实现证明↗DeflateBounds.leanZlibF/Proof/Api/DeflateBounds.lean实现证明↗DeflateFlush.leanZlibF/Proof/Api/DeflateFlush.lean实现证明↗DictionaryRoundtrip.leanZlibF/Proof/Api/DictionaryRoundtrip.lean实现证明↗GzRoundtrip.leanZlibF/Proof/Api/GzRoundtrip.lean实现证明↗GzipRoundtrip.leanZlibF/Proof/Api/GzipRoundtrip.lean实现证明↗HeaderRoundtrip.leanZlibF/Proof/Api/HeaderRoundtrip.lean实现证明↗HeapCleanup.leanZlibF/Proof/Api/HeapCleanup.lean实现证明↗Inflate.leanZlibF/Proof/Api/Inflate.lean实现证明↗InflateCausality.leanZlibF/Proof/Api/InflateCausality.lean实现证明↗InflateDictionary.leanZlibF/Proof/Api/InflateDictionary.lean实现证明↗QueryLayout.leanZlibF/Proof/Api/QueryLayout.lean实现证明↗Roundtrip.leanZlibF/Proof/Api/Roundtrip.lean实现证明↗ByteAddress.leanZlibF/Proof/ByteAddress.lean实现证明↗Api.leanZlibF/Proof/Format/Api.lean实现证明↗Deflate.leanZlibF/Proof/Format/Deflate.lean实现证明↗Dictionary.leanZlibF/Proof/Format/Dictionary.lean实现证明↗Huffman.leanZlibF/Proof/Format/Huffman.lean实现证明↗Token.leanZlibF/Proof/Format/Token.lean实现证明↗Wrapper.leanZlibF/Proof/Format/Wrapper.lean实现证明↗Index.leanZlibF/Proof/Index.lean实现证明↗PlatformMemory.leanZlibF/Proof/PlatformMemory.lean实现证明↗adler32.c.leanZlibF/Proof/adler32.c.lean实现证明↗adler32.c.public-any.leanZlibF/Proof/adler32.c.public-any.lean实现证明↗adler32.c.public-block.leanZlibF/Proof/adler32.c.public-block.lean实现证明↗adler32.c.public-one.leanZlibF/Proof/adler32.c.public-one.lean实现证明↗crc32.c.leanZlibF/Proof/crc32.c.lean实现证明↗crc32.c.views.leanZlibF/Proof/crc32.c.views.lean实现证明↗deflate.c.base.leanZlibF/Proof/deflate.c.base.lean实现证明↗deflate.c.engine.chains.leanZlibF/Proof/deflate.c.engine.chains.lean实现证明↗deflate.c.engine.hash.leanZlibF/Proof/deflate.c.engine.hash.lean实现证明↗deflate.c.engine.lmbody.leanZlibF/Proof/deflate.c.engine.lmbody.lean实现证明↗deflate.c.engine.lmcond.leanZlibF/Proof/deflate.c.engine.lmcond.lean实现证明↗deflate.c.engine.lminner.leanZlibF/Proof/deflate.c.engine.lminner.lean实现证明↗deflate.c.engine.lmmain.leanZlibF/Proof/deflate.c.engine.lmmain.lean实现证明↗deflate.c.engine.loops.leanZlibF/Proof/deflate.c.engine.loops.lean实现证明↗deflate.c.engine.macros.leanZlibF/Proof/deflate.c.engine.macros.lean实现证明↗deflate.c.engine.match.leanZlibF/Proof/deflate.c.engine.match.lean实现证明↗deflate.c.engine.readbuf.leanZlibF/Proof/deflate.c.engine.readbuf.lean实现证明↗deflate.c.engine.slide.leanZlibF/Proof/deflate.c.engine.slide.lean实现证明↗deflate.c.engine.window.leanZlibF/Proof/deflate.c.engine.window.lean实现证明↗deflate.c.init.cleanup.leanZlibF/Proof/deflate.c.init.cleanup.lean实现证明↗deflate.c.init.construct.leanZlibF/Proof/deflate.c.init.construct.lean实现证明↗deflate.c.init.default.leanZlibF/Proof/deflate.c.init.default.lean实现证明↗deflate.c.init.failure.leanZlibF/Proof/deflate.c.init.failure.lean实现证明↗deflate.c.init.frame.leanZlibF/Proof/deflate.c.init.frame.lean实现证明↗deflate.c.init.memory.leanZlibF/Proof/deflate.c.init.memory.lean实现证明↗deflate.c.init.storage.leanZlibF/Proof/deflate.c.init.storage.lean实现证明↗deflate.c.init.success.leanZlibF/Proof/deflate.c.init.success.lean实现证明↗deflate.c.life.bound.leanZlibF/Proof/deflate.c.life.bound.lean实现证明↗deflate.c.life.check.leanZlibF/Proof/deflate.c.life.check.lean实现证明↗deflate.c.life.end.leanZlibF/Proof/deflate.c.life.end.lean实现证明↗deflate.c.life.getdict.leanZlibF/Proof/deflate.c.life.getdict.lean实现证明↗deflate.c.life.reset.leanZlibF/Proof/deflate.c.life.reset.lean实现证明↗deflate.c.prime.leanZlibF/Proof/deflate.c.prime.lean实现证明↗deflate.c.public-getdict.leanZlibF/Proof/deflate.c.public-getdict.lean实现证明↗gzclose.c.leanZlibF/Proof/gzclose.c.lean实现证明↗gzfs.leanZlibF/Proof/gzfs.lean实现证明↗gzlib.c.base.leanZlibF/Proof/gzlib.c.base.lean实现证明↗gzlib.c.error.leanZlibF/Proof/gzlib.c.error.lean实现证明↗gzlib.c.open.leanZlibF/Proof/gzlib.c.open.lean实现证明↗gzlib.c.public-clearerr.leanZlibF/Proof/gzlib.c.public-clearerr.lean实现证明↗gzlib.c.rewind.leanZlibF/Proof/gzlib.c.rewind.lean实现证明↗gzlib.c.seek.leanZlibF/Proof/gzlib.c.seek.lean实现证明↗gzlib.c.simple.leanZlibF/Proof/gzlib.c.simple.lean实现证明↗gzread.c.close.leanZlibF/Proof/gzread.c.close.lean实现证明↗infback.c.back.leanZlibF/Proof/infback.c.back.lean实现证明↗infback.c.callbacks.leanZlibF/Proof/infback.c.callbacks.lean实现证明↗infback.c.end.leanZlibF/Proof/infback.c.end.lean实现证明↗infback.c.init.leanZlibF/Proof/infback.c.init.lean实现证明↗infback.c.inv.leanZlibF/Proof/infback.c.inv.lean实现证明↗infback.c.macros.leanZlibF/Proof/infback.c.macros.lean实现证明↗infback.c.pull.leanZlibF/Proof/infback.c.pull.lean实现证明↗infback.c.pure.leanZlibF/Proof/infback.c.pure.lean实现证明↗infback.c.room.leanZlibF/Proof/infback.c.room.lean实现证明↗infback.c.stored.leanZlibF/Proof/infback.c.stored.lean实现证明↗infback.c.wf.leanZlibF/Proof/infback.c.wf.lean实现证明↗inffast.c.advance.leanZlibF/Proof/inffast.c.advance.lean实现证明↗inffast.c.base.leanZlibF/Proof/inffast.c.base.lean实现证明↗inffast.c.body-origin.leanZlibF/Proof/inffast.c.body-origin.lean实现证明↗inffast.c.body-token.leanZlibF/Proof/inffast.c.body-token.lean实现证明↗inffast.c.body.leanZlibF/Proof/inffast.c.body.lean实现证明↗inffast.c.call-origin.leanZlibF/Proof/inffast.c.call-origin.lean实现证明↗inffast.c.copy.leanZlibF/Proof/inffast.c.copy.lean实现证明↗inffast.c.dist.leanZlibF/Proof/inffast.c.dist.lean实现证明↗inffast.c.distance-origin.leanZlibF/Proof/inffast.c.distance-origin.lean实现证明↗inffast.c.distance-result.leanZlibF/Proof/inffast.c.distance-result.lean实现证明↗inffast.c.distance-semantics.leanZlibF/Proof/inffast.c.distance-semantics.lean实现证明↗inffast.c.env.leanZlibF/Proof/inffast.c.env.lean实现证明↗inffast.c.final.leanZlibF/Proof/inffast.c.final.lean实现证明↗inffast.c.flags.leanZlibF/Proof/inffast.c.flags.lean实现证明↗inffast.c.frame.leanZlibF/Proof/inffast.c.frame.lean实现证明↗inffast.c.len.leanZlibF/Proof/inffast.c.len.lean实现证明↗inffast.c.length-semantics.leanZlibF/Proof/inffast.c.length-semantics.lean实现证明↗inffast.c.length-trace.leanZlibF/Proof/inffast.c.length-trace.lean实现证明↗inffast.c.loop.leanZlibF/Proof/inffast.c.loop.lean实现证明↗inffast.c.lp.leanZlibF/Proof/inffast.c.lp.lean实现证明↗inffast.c.match-history.leanZlibF/Proof/inffast.c.match-history.lean实现证明↗inffast.c.match.leanZlibF/Proof/inffast.c.match.lean实现证明↗inffast.c.message.leanZlibF/Proof/inffast.c.message.lean实现证明↗inffast.c.origin.leanZlibF/Proof/inffast.c.origin.lean实现证明↗inffast.c.pass.leanZlibF/Proof/inffast.c.pass.lean实现证明↗inffast.c.platform.leanZlibF/Proof/inffast.c.platform.lean实现证明↗inffast.c.sig.leanZlibF/Proof/inffast.c.sig.lean实现证明↗inffast.c.step1.leanZlibF/Proof/inffast.c.step1.lean实现证明↗inffast.c.tableok.leanZlibF/Proof/inffast.c.tableok.lean实现证明↗inflate.c.base.leanZlibF/Proof/inflate.c.base.lean实现证明↗inflate.c.dict.leanZlibF/Proof/inflate.c.dict.lean实现证明↗inflate.c.end.leanZlibF/Proof/inflate.c.end.lean实现证明↗inflate.c.hdr.leanZlibF/Proof/inflate.c.hdr.lean实现证明↗inflate.c.init.leanZlibF/Proof/inflate.c.init.lean实现证明↗inflate.c.input-cursor.leanZlibF/Proof/inflate.c.input-cursor.lean实现证明↗inflate.c.lookup-codes.leanZlibF/Proof/inflate.c.lookup-codes.lean实现证明↗inflate.c.lookup-loop.leanZlibF/Proof/inflate.c.lookup-loop.lean实现证明↗inflate.c.main.bits.leanZlibF/Proof/inflate.c.main.bits.lean实现证明↗inflate.c.main.check.leanZlibF/Proof/inflate.c.main.check.lean实现证明↗inflate.c.main.check0.leanZlibF/Proof/inflate.c.main.check0.lean实现证明↗inflate.c.main.common.leanZlibF/Proof/inflate.c.main.common.lean实现证明↗inflate.c.main.macros.leanZlibF/Proof/inflate.c.main.macros.lean实现证明↗inflate.c.main.simple.leanZlibF/Proof/inflate.c.main.simple.lean实现证明↗inflate.c.main.stored.leanZlibF/Proof/inflate.c.main.stored.lean实现证明↗inflate.c.main.stored2.leanZlibF/Proof/inflate.c.main.stored2.lean实现证明↗inflate.c.main.table.leanZlibF/Proof/inflate.c.main.table.lean实现证明↗inflate.c.main.table2.leanZlibF/Proof/inflate.c.main.table2.lean实现证明↗inflate.c.main.table3.leanZlibF/Proof/inflate.c.main.table3.lean实现证明↗inflate.c.main.table4.leanZlibF/Proof/inflate.c.main.table4.lean实现证明↗inflate.c.main.table5.leanZlibF/Proof/inflate.c.main.table5.lean实现证明↗inflate.c.main.table6.leanZlibF/Proof/inflate.c.main.table6.lean实现证明↗inflate.c.main.type.leanZlibF/Proof/inflate.c.main.type.lean实现证明↗inflate.c.main.xloop.leanZlibF/Proof/inflate.c.main.xloop.lean实现证明↗inflate.c.misc.leanZlibF/Proof/inflate.c.misc.lean实现证明↗inflate.c.misc2.leanZlibF/Proof/inflate.c.misc2.lean实现证明↗inflate.c.platform.leanZlibF/Proof/inflate.c.platform.lean实现证明↗inflate.c.public-getdict.leanZlibF/Proof/inflate.c.public-getdict.lean实现证明↗inflate.c.public-setdict-success.leanZlibF/Proof/inflate.c.public-setdict-success.lean实现证明↗inflate.c.public-setdict.leanZlibF/Proof/inflate.c.public-setdict.lean实现证明↗inflate.c.reset.leanZlibF/Proof/inflate.c.reset.lean实现证明↗inflate.c.ring.leanZlibF/Proof/inflate.c.ring.lean实现证明↗inflate.c.start.leanZlibF/Proof/inflate.c.start.lean实现证明↗inflate.c.sync.leanZlibF/Proof/inflate.c.sync.lean实现证明↗inflate.c.sync2.leanZlibF/Proof/inflate.c.sync2.lean实现证明↗inflate.c.sync3.leanZlibF/Proof/inflate.c.sync3.lean实现证明↗inflate.c.sync4.leanZlibF/Proof/inflate.c.sync4.lean实现证明↗inflate.c.uw.leanZlibF/Proof/inflate.c.uw.lean实现证明↗inflate.c.window-compose.leanZlibF/Proof/inflate.c.window-compose.lean实现证明↗inflate.c.window-general.leanZlibF/Proof/inflate.c.window-general.lean实现证明↗inflate.c.window-platform.leanZlibF/Proof/inflate.c.window-platform.lean实现证明↗inflate.c.window-public-mode.leanZlibF/Proof/inflate.c.window-public-mode.lean实现证明↗inflate.c.window-public-ring.leanZlibF/Proof/inflate.c.window-public-ring.lean实现证明↗inflate.c.window.leanZlibF/Proof/inflate.c.window.lean实现证明↗inflate.c.witness.leanZlibF/Proof/inflate.c.witness.lean实现证明↗inflate.c.xloop-rank.leanZlibF/Proof/inflate.c.xloop-rank.lean实现证明↗inftrees.c.base.leanZlibF/Proof/inftrees.c.base.lean实现证明↗inftrees.c.canon.leanZlibF/Proof/inftrees.c.canon.lean实现证明↗inftrees.c.canonbridge.leanZlibF/Proof/inftrees.c.canonbridge.lean实现证明↗inftrees.c.content.codes.leanZlibF/Proof/inftrees.c.content.codes.lean实现证明↗inftrees.c.content.data.leanZlibF/Proof/inftrees.c.content.data.lean实现证明↗inftrees.c.content.geometry.leanZlibF/Proof/inftrees.c.content.geometry.lean实现证明↗inftrees.c.content.leanZlibF/Proof/inftrees.c.content.lean实现证明↗inftrees.c.content.result.leanZlibF/Proof/inftrees.c.content.result.lean实现证明↗inftrees.c.content.tail.leanZlibF/Proof/inftrees.c.content.tail.lean实现证明↗inftrees.c.cover.fn.leanZlibF/Proof/inftrees.c.cover.fn.lean实现证明↗inftrees.c.cover.group.leanZlibF/Proof/inftrees.c.cover.group.lean实现证明↗inftrees.c.cover.leaf.leanZlibF/Proof/inftrees.c.cover.leaf.lean实现证明↗inftrees.c.cover.root.leanZlibF/Proof/inftrees.c.cover.root.lean实现证明↗inftrees.c.cover.stmt.leanZlibF/Proof/inftrees.c.cover.stmt.lean实现证明↗inftrees.c.cover.tile.leanZlibF/Proof/inftrees.c.cover.tile.lean实现证明↗inftrees.c.decode.frame.leanZlibF/Proof/inftrees.c.decode.frame.lean实现证明↗inftrees.c.decode.stability-rejection.leanZlibF/Proof/inftrees.c.decode.stability-rejection.lean实现证明↗inftrees.c.decoder-safe.leanZlibF/Proof/inftrees.c.decoder-safe.lean实现证明↗inftrees.c.final-layout.leanZlibF/Proof/inftrees.c.final-layout.lean实现证明↗inftrees.c.fixed.leanZlibF/Proof/inftrees.c.fixed.lean实现证明↗inftrees.c.geom.leanZlibF/Proof/inftrees.c.geom.lean实现证明↗inftrees.c.leanZlibF/Proof/inftrees.c.lean实现证明↗inftrees.c.link.leanZlibF/Proof/inftrees.c.link.lean实现证明↗inftrees.c.main.leanZlibF/Proof/inftrees.c.main.lean实现证明↗inftrees.c.math.leanZlibF/Proof/inftrees.c.math.lean实现证明↗inftrees.c.read-extent.leanZlibF/Proof/inftrees.c.read-extent.lean实现证明↗inftrees.c.spec.leanZlibF/Proof/inftrees.c.spec.lean实现证明↗inftrees.c.step.leanZlibF/Proof/inftrees.c.step.lean实现证明↗pointer-arithmetic.leanZlibF/Proof/pointer-arithmetic.lean实现证明↗public-adler-combine.leanZlibF/Proof/public-adler-combine.lean实现证明↗public-adler-update.leanZlibF/Proof/public-adler-update.lean实现证明↗public-compress-bound.leanZlibF/Proof/public-compress-bound.lean实现证明↗public-crc-combine.leanZlibF/Proof/public-crc-combine.lean实现证明↗public-crc-updates.leanZlibF/Proof/public-crc-updates.lean实现证明↗public-deflate-end.leanZlibF/Proof/public-deflate-end.lean实现证明↗public-deflate-getdict.leanZlibF/Proof/public-deflate-getdict.lean实现证明↗public-deflate-init.leanZlibF/Proof/public-deflate-init.lean实现证明↗public-deflate-reset-keep.leanZlibF/Proof/public-deflate-reset-keep.lean实现证明↗public-deflate-reset.leanZlibF/Proof/public-deflate-reset.lean实现证明↗public-deflate-small-queries.leanZlibF/Proof/public-deflate-small-queries.lean实现证明↗public-get-crc-table.leanZlibF/Proof/public-get-crc-table.lean实现证明↗public-gz-error.leanZlibF/Proof/public-gz-error.lean实现证明↗public-gz-offset.leanZlibF/Proof/public-gz-offset.lean实现证明↗public-gz-rewind.leanZlibF/Proof/public-gz-rewind.lean实现证明↗public-gzbuffer.leanZlibF/Proof/public-gzbuffer.lean实现证明↗public-gzeof.leanZlibF/Proof/public-gzeof.lean实现证明↗public-infback-end.leanZlibF/Proof/public-infback-end.lean实现证明↗public-infback-init.leanZlibF/Proof/public-infback-init.lean实现证明↗public-inflate-end.leanZlibF/Proof/public-inflate-end.lean实现证明↗public-inflate-getdict.leanZlibF/Proof/public-inflate-getdict.lean实现证明↗public-inflate-header.leanZlibF/Proof/public-inflate-header.lean实现证明↗public-inflate-init.leanZlibF/Proof/public-inflate-init.lean实现证明↗public-inflate-mark.leanZlibF/Proof/public-inflate-mark.lean实现证明↗public-inflate-prime.leanZlibF/Proof/public-inflate-prime.lean实现证明↗public-inflate-reset-keep.leanZlibF/Proof/public-inflate-reset-keep.lean实现证明↗public-inflate-reset.leanZlibF/Proof/public-inflate-reset.lean实现证明↗public-inflate-reset2.leanZlibF/Proof/public-inflate-reset2.lean实现证明↗public-inflate-setdict.leanZlibF/Proof/public-inflate-setdict.lean实现证明↗public-inflate-small-queries.leanZlibF/Proof/public-inflate-small-queries.lean实现证明↗public-zerror.leanZlibF/Proof/public-zerror.lean实现证明↗public-zlib-compile-flags.leanZlibF/Proof/public-zlib-compile-flags.lean实现证明↗public-zlib-version.leanZlibF/Proof/public-zlib-version.lean实现证明↗trees.c.align.leanZlibF/Proof/trees.c.align.lean实现证明↗trees.c.arrays.leanZlibF/Proof/trees.c.arrays.lean实现证明↗trees.c.bits.leanZlibF/Proof/trees.c.bits.lean实现证明↗trees.c.bl-support.leanZlibF/Proof/trees.c.bl-support.lean实现证明↗trees.c.bl-tree.leanZlibF/Proof/trees.c.bl-tree.lean实现证明↗trees.c.block.leanZlibF/Proof/trees.c.block.lean实现证明↗trees.c.build.complete.leanZlibF/Proof/trees.c.build.complete.lean实现证明↗trees.c.build.emit.leanZlibF/Proof/trees.c.build.emit.lean实现证明↗trees.c.build.force.leanZlibF/Proof/trees.c.build.force.lean实现证明↗trees.c.build.forest.leanZlibF/Proof/trees.c.build.forest.lean实现证明↗trees.c.build.format.leanZlibF/Proof/trees.c.build.format.lean实现证明↗trees.c.build.frame.leanZlibF/Proof/trees.c.build.frame.lean实现证明↗trees.c.build.heapify.leanZlibF/Proof/trees.c.build.heapify.lean实现证明↗trees.c.build.leaves.leanZlibF/Proof/trees.c.build.leaves.lean实现证明↗trees.c.build.lengths.leanZlibF/Proof/trees.c.build.lengths.lean实现证明↗trees.c.build.merge.leanZlibF/Proof/trees.c.build.merge.lean实现证明↗trees.c.build.order.leanZlibF/Proof/trees.c.build.order.lean实现证明↗trees.c.build.scan.leanZlibF/Proof/trees.c.build.scan.lean实现证明↗trees.c.build.static.leanZlibF/Proof/trees.c.build.static.lean实现证明↗trees.c.build.support.leanZlibF/Proof/trees.c.build.support.lean实现证明↗trees.c.build.tail.leanZlibF/Proof/trees.c.build.tail.lean实现证明↗trees.c.codes.leanZlibF/Proof/trees.c.codes.lean实现证明↗trees.c.emit-state.leanZlibF/Proof/trees.c.emit-state.lean实现证明↗trees.c.emit.leanZlibF/Proof/trees.c.emit.lean实现证明↗trees.c.heap.base.leanZlibF/Proof/trees.c.heap.base.lean实现证明↗trees.c.heap.gbclk.leanZlibF/Proof/trees.c.heap.gbclk.lean实现证明↗trees.c.heap.gbdef.leanZlibF/Proof/trees.c.heap.gbdef.lean实现证明↗trees.c.heap.gbfix.leanZlibF/Proof/trees.c.heap.gbfix.lean实现证明↗trees.c.heap.gbmath.leanZlibF/Proof/trees.c.heap.gbmath.lean实现证明↗trees.c.heap.gbp1.leanZlibF/Proof/trees.c.heap.gbp1.lean实现证明↗trees.c.heap.gbre.leanZlibF/Proof/trees.c.heap.gbre.lean实现证明↗trees.c.heap.gbsym.leanZlibF/Proof/trees.c.heap.gbsym.lean实现证明↗trees.c.heap.gbtop.leanZlibF/Proof/trees.c.heap.gbtop.lean实现证明↗trees.c.heap.gbtree.leanZlibF/Proof/trees.c.heap.gbtree.lean实现证明↗trees.c.heap.ord.leanZlibF/Proof/trees.c.heap.ord.lean实现证明↗trees.c.heap.pq.leanZlibF/Proof/trees.c.heap.pq.lean实现证明↗trees.c.heap.pqrun.leanZlibF/Proof/trees.c.heap.pqrun.lean实现证明↗trees.c.inv.leanZlibF/Proof/trees.c.inv.lean实现证明↗trees.c.monad.leanZlibF/Proof/trees.c.monad.lean实现证明↗trees.c.reverse.leanZlibF/Proof/trees.c.reverse.lean实现证明↗trees.c.runs.leanZlibF/Proof/trees.c.runs.lean实现证明↗trees.c.scan-tree.leanZlibF/Proof/trees.c.scan-tree.lean实现证明↗trees.c.send-support.leanZlibF/Proof/trees.c.send-support.lean实现证明↗trees.c.send-tree.leanZlibF/Proof/trees.c.send-tree.lean实现证明↗trees.c.tally-support.leanZlibF/Proof/trees.c.tally-support.lean实现证明↗trees.c.tally.leanZlibF/Proof/trees.c.tally.lean实现证明↗zutil.c.leanZlibF/Proof/zutil.c.lean实现证明↗Address.leanZlibF/Runtime/Address.lean运行时模型↗Alloc.leanZlibF/Runtime/Alloc.lean运行时模型↗Libc.leanZlibF/Runtime/Libc.lean运行时模型↗LibcTables.leanZlibF/Runtime/LibcTables.lean运行时模型↗Monad.leanZlibF/Runtime/Monad.lean运行时模型↗Ptr.leanZlibF/Runtime/Ptr.lean运行时模型↗Schema.leanZlibF/Runtime/Schema.lean运行时模型↗Space.leanZlibF/Runtime/Space.lean运行时模型↗Tables.leanZlibF/Runtime/Tables.lean运行时模型↗Basic.leanZlibF/Spec/Api/Basic.lean函数与格式规格↗Compress.leanZlibF/Spec/Api/Compress.lean函数与格式规格↗Concrete.leanZlibF/Spec/Api/Concrete.lean函数与格式规格↗Deflate.leanZlibF/Spec/Api/Deflate.lean函数与格式规格↗Examples.leanZlibF/Spec/Api/Examples.lean函数与格式规格↗Goals.leanZlibF/Spec/Api/Goals.lean函数与格式规格↗Gz.leanZlibF/Spec/Api/Gz.lean函数与格式规格↗Header.leanZlibF/Spec/Api/Header.lean函数与格式规格↗Iface.leanZlibF/Spec/Api/Iface.lean函数与格式规格↗Inflate.leanZlibF/Spec/Api/Inflate.lean函数与格式规格↗Run.leanZlibF/Spec/Api/Run.lean函数与格式规格↗Api.leanZlibF/Spec/Api.lean函数与格式规格↗ByteAddress.leanZlibF/Spec/ByteAddress.lean函数与格式规格↗Crc32ByteViews.leanZlibF/Spec/Crc32ByteViews.lean函数与格式规格↗Bits.leanZlibF/Spec/Format/Bits.lean函数与格式规格↗Checksum.leanZlibF/Spec/Format/Checksum.lean函数与格式规格↗Deflate.leanZlibF/Spec/Format/Deflate.lean函数与格式规格↗Examples.leanZlibF/Spec/Format/Examples.lean函数与格式规格↗Huffman.leanZlibF/Spec/Format/Huffman.lean函数与格式规格↗Token.leanZlibF/Spec/Format/Token.lean函数与格式规格↗Wrapper.leanZlibF/Spec/Format/Wrapper.lean函数与格式规格↗Format.leanZlibF/Spec/Format.lean函数与格式规格↗InflateDecodeTableFrame.leanZlibF/Spec/InflateDecodeTableFrame.lean函数与格式规格↗InflateDecodeTableInvariant.leanZlibF/Spec/InflateDecodeTableInvariant.lean函数与格式规格↗InflateDecodeTableRejection.leanZlibF/Spec/InflateDecodeTableRejection.lean函数与格式规格↗InflateDecodeTableSemantics.leanZlibF/Spec/InflateDecodeTableSemantics.lean函数与格式规格↗InflateDecodeTableShort.leanZlibF/Spec/InflateDecodeTableShort.lean函数与格式规格↗InflateDecodeTableSoundness.leanZlibF/Spec/InflateDecodeTableSoundness.lean函数与格式规格↗InflateDecodeTableStability.leanZlibF/Spec/InflateDecodeTableStability.lean函数与格式规格↗InflateFast.leanZlibF/Spec/InflateFast.lean函数与格式规格↗InflateFastBodyOrigin.leanZlibF/Spec/InflateFastBodyOrigin.lean函数与格式规格↗InflateFastBodyToken.leanZlibF/Spec/InflateFastBodyToken.lean函数与格式规格↗InflateFastCallOrigin.leanZlibF/Spec/InflateFastCallOrigin.lean函数与格式规格↗InflateFastDistanceOrigin.leanZlibF/Spec/InflateFastDistanceOrigin.lean函数与格式规格↗InflateFastDistanceResult.leanZlibF/Spec/InflateFastDistanceResult.lean函数与格式规格↗InflateFastDistanceSemantics.leanZlibF/Spec/InflateFastDistanceSemantics.lean函数与格式规格↗InflateFastLengthSemantics.leanZlibF/Spec/InflateFastLengthSemantics.lean函数与格式规格↗InflateFastLengthTrace.leanZlibF/Spec/InflateFastLengthTrace.lean函数与格式规格↗InflateFastMatchHistory.leanZlibF/Spec/InflateFastMatchHistory.lean函数与格式规格↗InflateFastOrigin.leanZlibF/Spec/InflateFastOrigin.lean函数与格式规格↗InflateFastPlatform.leanZlibF/Spec/InflateFastPlatform.lean函数与格式规格↗InflateFastTableFlags.leanZlibF/Spec/InflateFastTableFlags.lean函数与格式规格↗InflateRootTable.leanZlibF/Spec/InflateRootTable.lean函数与格式规格↗InflateSubtable.leanZlibF/Spec/InflateSubtable.lean函数与格式规格↗InflateTableContent.leanZlibF/Spec/InflateTableContent.lean函数与格式规格↗InflateTableExtent.leanZlibF/Spec/InflateTableExtent.lean函数与格式规格↗InflateTableSafety.leanZlibF/Spec/InflateTableSafety.lean函数与格式规格↗PlatformMemory.leanZlibF/Spec/PlatformMemory.lean函数与格式规格↗Back.leanZlibF/Spec/Public/Back.lean函数与格式规格↗Calls.leanZlibF/Spec/Public/Calls.lean函数与格式规格↗Checksums.leanZlibF/Spec/Public/Checksums.lean函数与格式规格↗Copy.leanZlibF/Spec/Public/Copy.lean函数与格式规格↗Domains.leanZlibF/Spec/Public/Domains.lean函数与格式规格↗GzClose.leanZlibF/Spec/Public/GzClose.lean函数与格式规格↗GzControl.leanZlibF/Spec/Public/GzControl.lean函数与格式规格↗GzOpen.leanZlibF/Spec/Public/GzOpen.lean函数与格式规格↗GzRead.leanZlibF/Spec/Public/GzRead.lean函数与格式规格↗GzState.leanZlibF/Spec/Public/GzState.lean函数与格式规格↗GzTrace.leanZlibF/Spec/Public/GzTrace.lean函数与格式规格↗GzWrite.leanZlibF/Spec/Public/GzWrite.lean函数与格式规格↗History.leanZlibF/Spec/Public/History.lean函数与格式规格↗Initialisation.leanZlibF/Spec/Public/Initialisation.lean函数与格式规格↗Lifecycle.leanZlibF/Spec/Public/Lifecycle.lean函数与格式规格↗Memory.leanZlibF/Spec/Public/Memory.lean函数与格式规格↗Queries.leanZlibF/Spec/Public/Queries.lean函数与格式规格↗Sequences.leanZlibF/Spec/Public/Sequences.lean函数与格式规格↗StreamQueries.leanZlibF/Spec/Public/StreamQueries.lean函数与格式规格↗Streams.leanZlibF/Spec/Public/Streams.lean函数与格式规格↗Utilities.leanZlibF/Spec/Public/Utilities.lean函数与格式规格↗adler32.c.leanZlibF/Zlib/adler32.c.leanC 源码翻译↗compress.c.leanZlibF/Zlib/compress.c.leanC 源码翻译↗crc32.c.leanZlibF/Zlib/crc32.c.leanC 源码翻译↗crc32.h.leanZlibF/Zlib/crc32.h.leanC 源码翻译↗deflate.c.leanZlibF/Zlib/deflate.c.leanC 源码翻译↗deflate_base.c.leanZlibF/Zlib/deflate_base.c.leanC 源码翻译↗deflate_strategies.c.leanZlibF/Zlib/deflate_strategies.c.leanC 源码翻译↗gzclose.c.leanZlibF/Zlib/gzclose.c.leanC 源码翻译↗gzfs.leanZlibF/Zlib/gzfs.leanC 源码翻译↗gzguts.h.leanZlibF/Zlib/gzguts.h.leanC 源码翻译↗gzlib.c.leanZlibF/Zlib/gzlib.c.leanC 源码翻译↗gzread.c.leanZlibF/Zlib/gzread.c.leanC 源码翻译↗gzwrite.c.leanZlibF/Zlib/gzwrite.c.leanC 源码翻译↗infback.c.leanZlibF/Zlib/infback.c.leanC 源码翻译↗inffast.c.leanZlibF/Zlib/inffast.c.leanC 源码翻译↗inffixed.h.leanZlibF/Zlib/inffixed.h.leanC 源码翻译↗inflate.c.leanZlibF/Zlib/inflate.c.leanC 源码翻译↗inftrees.c.leanZlibF/Zlib/inftrees.c.leanC 源码翻译↗trees.c.leanZlibF/Zlib/trees.c.leanC 源码翻译↗uncompr.c.leanZlibF/Zlib/uncompr.c.leanC 源码翻译↗zutil.c.leanZlibF/Zlib/zutil.c.leanC 源码翻译↗ZlibF.leanZlibF.lean模块入口↗Gz.leantests/lean/Driver/Gz.leanlean↗gz-seek-mode.leantests/verification/counterexamples/gz-seek-mode.leanverification↗inflate-init2-table-shape.leantests/verification/counterexamples/inflate-init2-table-shape.leanverification↗crc-static-address.leantests/verification/regressions/crc-static-address.leanverification↗没有匹配模块。