REFERENCE / ZLIB × LEAN
Lean source and proof bodies
Find Lean modules by role: implementation proofs, specifications, mathematics, the runtime model, or C translation. Search by module path or declaration name.
DeflateBlIndex.leanZlibF/Math/DeflateBlIndex.leanMath↗DeflateCodes.leanZlibF/Math/DeflateCodes.leanMath↗DeflateForest.leanZlibF/Math/DeflateForest.leanMath↗DeflateHeap.leanZlibF/Math/DeflateHeap.leanMath↗DeflateHeapRemove.leanZlibF/Math/DeflateHeapRemove.leanMath↗DeflateKraft.leanZlibF/Math/DeflateKraft.leanMath↗DeflateRunSupport.leanZlibF/Math/DeflateRunSupport.leanMath↗DeflateTreeForce.leanZlibF/Math/DeflateTreeForce.leanMath↗DeflateTreeScan.leanZlibF/Math/DeflateTreeScan.leanMath↗InflateFastMatchHistory.leanZlibF/Math/InflateFastMatchHistory.leanMath↗InflatePrefixes.leanZlibF/Math/InflatePrefixes.leanMath↗InflateTableCoverage.leanZlibF/Math/InflateTableCoverage.leanMath↗InflateTableGeometry.leanZlibF/Math/InflateTableGeometry.leanMath↗LZ77Copy.leanZlibF/Math/LZ77Copy.leanMath↗LZ77CopySpec.leanZlibF/Math/LZ77CopySpec.leanMath↗LZ77History.leanZlibF/Math/LZ77History.leanMath↗LZ77HistorySpec.leanZlibF/Math/LZ77HistorySpec.leanMath↗Compress.leanZlibF/Proof/Api/Compress.leanProof↗CompressBoundary.leanZlibF/Proof/Api/CompressBoundary.leanProof↗CompressFailure.leanZlibF/Proof/Api/CompressFailure.leanProof↗CompressRoundtrip.leanZlibF/Proof/Api/CompressRoundtrip.leanProof↗Concrete.leanZlibF/Proof/Api/Concrete.leanProof↗Deflate.leanZlibF/Proof/Api/Deflate.leanProof↗DeflateBounds.leanZlibF/Proof/Api/DeflateBounds.leanProof↗DeflateFlush.leanZlibF/Proof/Api/DeflateFlush.leanProof↗DictionaryRoundtrip.leanZlibF/Proof/Api/DictionaryRoundtrip.leanProof↗GzRoundtrip.leanZlibF/Proof/Api/GzRoundtrip.leanProof↗GzipRoundtrip.leanZlibF/Proof/Api/GzipRoundtrip.leanProof↗HeaderRoundtrip.leanZlibF/Proof/Api/HeaderRoundtrip.leanProof↗HeapCleanup.leanZlibF/Proof/Api/HeapCleanup.leanProof↗Inflate.leanZlibF/Proof/Api/Inflate.leanProof↗InflateCausality.leanZlibF/Proof/Api/InflateCausality.leanProof↗InflateDictionary.leanZlibF/Proof/Api/InflateDictionary.leanProof↗QueryLayout.leanZlibF/Proof/Api/QueryLayout.leanProof↗Roundtrip.leanZlibF/Proof/Api/Roundtrip.leanProof↗ByteAddress.leanZlibF/Proof/ByteAddress.leanProof↗Api.leanZlibF/Proof/Format/Api.leanProof↗Deflate.leanZlibF/Proof/Format/Deflate.leanProof↗Dictionary.leanZlibF/Proof/Format/Dictionary.leanProof↗Huffman.leanZlibF/Proof/Format/Huffman.leanProof↗Token.leanZlibF/Proof/Format/Token.leanProof↗Wrapper.leanZlibF/Proof/Format/Wrapper.leanProof↗Index.leanZlibF/Proof/Index.leanProof↗PlatformMemory.leanZlibF/Proof/PlatformMemory.leanProof↗adler32.c.leanZlibF/Proof/adler32.c.leanProof↗adler32.c.public-any.leanZlibF/Proof/adler32.c.public-any.leanProof↗adler32.c.public-block.leanZlibF/Proof/adler32.c.public-block.leanProof↗adler32.c.public-one.leanZlibF/Proof/adler32.c.public-one.leanProof↗crc32.c.leanZlibF/Proof/crc32.c.leanProof↗crc32.c.views.leanZlibF/Proof/crc32.c.views.leanProof↗deflate.c.base.leanZlibF/Proof/deflate.c.base.leanProof↗deflate.c.engine.chains.leanZlibF/Proof/deflate.c.engine.chains.leanProof↗deflate.c.engine.hash.leanZlibF/Proof/deflate.c.engine.hash.leanProof↗deflate.c.engine.lmbody.leanZlibF/Proof/deflate.c.engine.lmbody.leanProof↗deflate.c.engine.lmcond.leanZlibF/Proof/deflate.c.engine.lmcond.leanProof↗deflate.c.engine.lminner.leanZlibF/Proof/deflate.c.engine.lminner.leanProof↗deflate.c.engine.lmmain.leanZlibF/Proof/deflate.c.engine.lmmain.leanProof↗deflate.c.engine.loops.leanZlibF/Proof/deflate.c.engine.loops.leanProof↗deflate.c.engine.macros.leanZlibF/Proof/deflate.c.engine.macros.leanProof↗deflate.c.engine.match.leanZlibF/Proof/deflate.c.engine.match.leanProof↗deflate.c.engine.readbuf.leanZlibF/Proof/deflate.c.engine.readbuf.leanProof↗deflate.c.engine.slide.leanZlibF/Proof/deflate.c.engine.slide.leanProof↗deflate.c.engine.window.leanZlibF/Proof/deflate.c.engine.window.leanProof↗deflate.c.init.cleanup.leanZlibF/Proof/deflate.c.init.cleanup.leanProof↗deflate.c.init.construct.leanZlibF/Proof/deflate.c.init.construct.leanProof↗deflate.c.init.default.leanZlibF/Proof/deflate.c.init.default.leanProof↗deflate.c.init.failure.leanZlibF/Proof/deflate.c.init.failure.leanProof↗deflate.c.init.frame.leanZlibF/Proof/deflate.c.init.frame.leanProof↗deflate.c.init.memory.leanZlibF/Proof/deflate.c.init.memory.leanProof↗deflate.c.init.storage.leanZlibF/Proof/deflate.c.init.storage.leanProof↗deflate.c.init.success.leanZlibF/Proof/deflate.c.init.success.leanProof↗deflate.c.life.bound.leanZlibF/Proof/deflate.c.life.bound.leanProof↗deflate.c.life.check.leanZlibF/Proof/deflate.c.life.check.leanProof↗deflate.c.life.end.leanZlibF/Proof/deflate.c.life.end.leanProof↗deflate.c.life.getdict.leanZlibF/Proof/deflate.c.life.getdict.leanProof↗deflate.c.life.reset.leanZlibF/Proof/deflate.c.life.reset.leanProof↗deflate.c.prime.leanZlibF/Proof/deflate.c.prime.leanProof↗deflate.c.public-getdict.leanZlibF/Proof/deflate.c.public-getdict.leanProof↗gzclose.c.leanZlibF/Proof/gzclose.c.leanProof↗gzfs.leanZlibF/Proof/gzfs.leanProof↗gzlib.c.base.leanZlibF/Proof/gzlib.c.base.leanProof↗gzlib.c.error.leanZlibF/Proof/gzlib.c.error.leanProof↗gzlib.c.open.leanZlibF/Proof/gzlib.c.open.leanProof↗gzlib.c.public-clearerr.leanZlibF/Proof/gzlib.c.public-clearerr.leanProof↗gzlib.c.rewind.leanZlibF/Proof/gzlib.c.rewind.leanProof↗gzlib.c.seek.leanZlibF/Proof/gzlib.c.seek.leanProof↗gzlib.c.simple.leanZlibF/Proof/gzlib.c.simple.leanProof↗gzread.c.close.leanZlibF/Proof/gzread.c.close.leanProof↗infback.c.back.leanZlibF/Proof/infback.c.back.leanProof↗infback.c.callbacks.leanZlibF/Proof/infback.c.callbacks.leanProof↗infback.c.end.leanZlibF/Proof/infback.c.end.leanProof↗infback.c.init.leanZlibF/Proof/infback.c.init.leanProof↗infback.c.inv.leanZlibF/Proof/infback.c.inv.leanProof↗infback.c.macros.leanZlibF/Proof/infback.c.macros.leanProof↗infback.c.pull.leanZlibF/Proof/infback.c.pull.leanProof↗infback.c.pure.leanZlibF/Proof/infback.c.pure.leanProof↗infback.c.room.leanZlibF/Proof/infback.c.room.leanProof↗infback.c.stored.leanZlibF/Proof/infback.c.stored.leanProof↗infback.c.wf.leanZlibF/Proof/infback.c.wf.leanProof↗inffast.c.advance.leanZlibF/Proof/inffast.c.advance.leanProof↗inffast.c.base.leanZlibF/Proof/inffast.c.base.leanProof↗inffast.c.body-origin.leanZlibF/Proof/inffast.c.body-origin.leanProof↗inffast.c.body-token.leanZlibF/Proof/inffast.c.body-token.leanProof↗inffast.c.body.leanZlibF/Proof/inffast.c.body.leanProof↗inffast.c.call-origin.leanZlibF/Proof/inffast.c.call-origin.leanProof↗inffast.c.copy.leanZlibF/Proof/inffast.c.copy.leanProof↗inffast.c.dist.leanZlibF/Proof/inffast.c.dist.leanProof↗inffast.c.distance-origin.leanZlibF/Proof/inffast.c.distance-origin.leanProof↗inffast.c.distance-result.leanZlibF/Proof/inffast.c.distance-result.leanProof↗inffast.c.distance-semantics.leanZlibF/Proof/inffast.c.distance-semantics.leanProof↗inffast.c.env.leanZlibF/Proof/inffast.c.env.leanProof↗inffast.c.final.leanZlibF/Proof/inffast.c.final.leanProof↗inffast.c.flags.leanZlibF/Proof/inffast.c.flags.leanProof↗inffast.c.frame.leanZlibF/Proof/inffast.c.frame.leanProof↗inffast.c.len.leanZlibF/Proof/inffast.c.len.leanProof↗inffast.c.length-semantics.leanZlibF/Proof/inffast.c.length-semantics.leanProof↗inffast.c.length-trace.leanZlibF/Proof/inffast.c.length-trace.leanProof↗inffast.c.loop.leanZlibF/Proof/inffast.c.loop.leanProof↗inffast.c.lp.leanZlibF/Proof/inffast.c.lp.leanProof↗inffast.c.match-history.leanZlibF/Proof/inffast.c.match-history.leanProof↗inffast.c.match.leanZlibF/Proof/inffast.c.match.leanProof↗inffast.c.message.leanZlibF/Proof/inffast.c.message.leanProof↗inffast.c.origin.leanZlibF/Proof/inffast.c.origin.leanProof↗inffast.c.pass.leanZlibF/Proof/inffast.c.pass.leanProof↗inffast.c.platform.leanZlibF/Proof/inffast.c.platform.leanProof↗inffast.c.sig.leanZlibF/Proof/inffast.c.sig.leanProof↗inffast.c.step1.leanZlibF/Proof/inffast.c.step1.leanProof↗inffast.c.tableok.leanZlibF/Proof/inffast.c.tableok.leanProof↗inflate.c.base.leanZlibF/Proof/inflate.c.base.leanProof↗inflate.c.dict.leanZlibF/Proof/inflate.c.dict.leanProof↗inflate.c.end.leanZlibF/Proof/inflate.c.end.leanProof↗inflate.c.hdr.leanZlibF/Proof/inflate.c.hdr.leanProof↗inflate.c.init.leanZlibF/Proof/inflate.c.init.leanProof↗inflate.c.input-cursor.leanZlibF/Proof/inflate.c.input-cursor.leanProof↗inflate.c.lookup-codes.leanZlibF/Proof/inflate.c.lookup-codes.leanProof↗inflate.c.lookup-loop.leanZlibF/Proof/inflate.c.lookup-loop.leanProof↗inflate.c.main.bits.leanZlibF/Proof/inflate.c.main.bits.leanProof↗inflate.c.main.check.leanZlibF/Proof/inflate.c.main.check.leanProof↗inflate.c.main.check0.leanZlibF/Proof/inflate.c.main.check0.leanProof↗inflate.c.main.common.leanZlibF/Proof/inflate.c.main.common.leanProof↗inflate.c.main.macros.leanZlibF/Proof/inflate.c.main.macros.leanProof↗inflate.c.main.simple.leanZlibF/Proof/inflate.c.main.simple.leanProof↗inflate.c.main.stored.leanZlibF/Proof/inflate.c.main.stored.leanProof↗inflate.c.main.stored2.leanZlibF/Proof/inflate.c.main.stored2.leanProof↗inflate.c.main.table.leanZlibF/Proof/inflate.c.main.table.leanProof↗inflate.c.main.table2.leanZlibF/Proof/inflate.c.main.table2.leanProof↗inflate.c.main.table3.leanZlibF/Proof/inflate.c.main.table3.leanProof↗inflate.c.main.table4.leanZlibF/Proof/inflate.c.main.table4.leanProof↗inflate.c.main.table5.leanZlibF/Proof/inflate.c.main.table5.leanProof↗inflate.c.main.table6.leanZlibF/Proof/inflate.c.main.table6.leanProof↗inflate.c.main.type.leanZlibF/Proof/inflate.c.main.type.leanProof↗inflate.c.main.xloop.leanZlibF/Proof/inflate.c.main.xloop.leanProof↗inflate.c.misc.leanZlibF/Proof/inflate.c.misc.leanProof↗inflate.c.misc2.leanZlibF/Proof/inflate.c.misc2.leanProof↗inflate.c.platform.leanZlibF/Proof/inflate.c.platform.leanProof↗inflate.c.public-getdict.leanZlibF/Proof/inflate.c.public-getdict.leanProof↗inflate.c.public-setdict-success.leanZlibF/Proof/inflate.c.public-setdict-success.leanProof↗inflate.c.public-setdict.leanZlibF/Proof/inflate.c.public-setdict.leanProof↗inflate.c.reset.leanZlibF/Proof/inflate.c.reset.leanProof↗inflate.c.ring.leanZlibF/Proof/inflate.c.ring.leanProof↗inflate.c.start.leanZlibF/Proof/inflate.c.start.leanProof↗inflate.c.sync.leanZlibF/Proof/inflate.c.sync.leanProof↗inflate.c.sync2.leanZlibF/Proof/inflate.c.sync2.leanProof↗inflate.c.sync3.leanZlibF/Proof/inflate.c.sync3.leanProof↗inflate.c.sync4.leanZlibF/Proof/inflate.c.sync4.leanProof↗inflate.c.uw.leanZlibF/Proof/inflate.c.uw.leanProof↗inflate.c.window-compose.leanZlibF/Proof/inflate.c.window-compose.leanProof↗inflate.c.window-general.leanZlibF/Proof/inflate.c.window-general.leanProof↗inflate.c.window-platform.leanZlibF/Proof/inflate.c.window-platform.leanProof↗inflate.c.window-public-mode.leanZlibF/Proof/inflate.c.window-public-mode.leanProof↗inflate.c.window-public-ring.leanZlibF/Proof/inflate.c.window-public-ring.leanProof↗inflate.c.window.leanZlibF/Proof/inflate.c.window.leanProof↗inflate.c.witness.leanZlibF/Proof/inflate.c.witness.leanProof↗inflate.c.xloop-rank.leanZlibF/Proof/inflate.c.xloop-rank.leanProof↗inftrees.c.base.leanZlibF/Proof/inftrees.c.base.leanProof↗inftrees.c.canon.leanZlibF/Proof/inftrees.c.canon.leanProof↗inftrees.c.canonbridge.leanZlibF/Proof/inftrees.c.canonbridge.leanProof↗inftrees.c.content.codes.leanZlibF/Proof/inftrees.c.content.codes.leanProof↗inftrees.c.content.data.leanZlibF/Proof/inftrees.c.content.data.leanProof↗inftrees.c.content.geometry.leanZlibF/Proof/inftrees.c.content.geometry.leanProof↗inftrees.c.content.leanZlibF/Proof/inftrees.c.content.leanProof↗inftrees.c.content.result.leanZlibF/Proof/inftrees.c.content.result.leanProof↗inftrees.c.content.tail.leanZlibF/Proof/inftrees.c.content.tail.leanProof↗inftrees.c.cover.fn.leanZlibF/Proof/inftrees.c.cover.fn.leanProof↗inftrees.c.cover.group.leanZlibF/Proof/inftrees.c.cover.group.leanProof↗inftrees.c.cover.leaf.leanZlibF/Proof/inftrees.c.cover.leaf.leanProof↗inftrees.c.cover.root.leanZlibF/Proof/inftrees.c.cover.root.leanProof↗inftrees.c.cover.stmt.leanZlibF/Proof/inftrees.c.cover.stmt.leanProof↗inftrees.c.cover.tile.leanZlibF/Proof/inftrees.c.cover.tile.leanProof↗inftrees.c.decode.frame.leanZlibF/Proof/inftrees.c.decode.frame.leanProof↗inftrees.c.decode.stability-rejection.leanZlibF/Proof/inftrees.c.decode.stability-rejection.leanProof↗inftrees.c.decoder-safe.leanZlibF/Proof/inftrees.c.decoder-safe.leanProof↗inftrees.c.final-layout.leanZlibF/Proof/inftrees.c.final-layout.leanProof↗inftrees.c.fixed.leanZlibF/Proof/inftrees.c.fixed.leanProof↗inftrees.c.geom.leanZlibF/Proof/inftrees.c.geom.leanProof↗inftrees.c.leanZlibF/Proof/inftrees.c.leanProof↗inftrees.c.link.leanZlibF/Proof/inftrees.c.link.leanProof↗inftrees.c.main.leanZlibF/Proof/inftrees.c.main.leanProof↗inftrees.c.math.leanZlibF/Proof/inftrees.c.math.leanProof↗inftrees.c.read-extent.leanZlibF/Proof/inftrees.c.read-extent.leanProof↗inftrees.c.spec.leanZlibF/Proof/inftrees.c.spec.leanProof↗inftrees.c.step.leanZlibF/Proof/inftrees.c.step.leanProof↗pointer-arithmetic.leanZlibF/Proof/pointer-arithmetic.leanProof↗public-adler-combine.leanZlibF/Proof/public-adler-combine.leanProof↗public-adler-update.leanZlibF/Proof/public-adler-update.leanProof↗public-compress-bound.leanZlibF/Proof/public-compress-bound.leanProof↗public-crc-combine.leanZlibF/Proof/public-crc-combine.leanProof↗public-crc-updates.leanZlibF/Proof/public-crc-updates.leanProof↗public-deflate-end.leanZlibF/Proof/public-deflate-end.leanProof↗public-deflate-getdict.leanZlibF/Proof/public-deflate-getdict.leanProof↗public-deflate-init.leanZlibF/Proof/public-deflate-init.leanProof↗public-deflate-reset-keep.leanZlibF/Proof/public-deflate-reset-keep.leanProof↗public-deflate-reset.leanZlibF/Proof/public-deflate-reset.leanProof↗public-deflate-small-queries.leanZlibF/Proof/public-deflate-small-queries.leanProof↗public-get-crc-table.leanZlibF/Proof/public-get-crc-table.leanProof↗public-gz-error.leanZlibF/Proof/public-gz-error.leanProof↗public-gz-offset.leanZlibF/Proof/public-gz-offset.leanProof↗public-gz-rewind.leanZlibF/Proof/public-gz-rewind.leanProof↗public-gzbuffer.leanZlibF/Proof/public-gzbuffer.leanProof↗public-gzeof.leanZlibF/Proof/public-gzeof.leanProof↗public-infback-end.leanZlibF/Proof/public-infback-end.leanProof↗public-infback-init.leanZlibF/Proof/public-infback-init.leanProof↗public-inflate-end.leanZlibF/Proof/public-inflate-end.leanProof↗public-inflate-getdict.leanZlibF/Proof/public-inflate-getdict.leanProof↗public-inflate-header.leanZlibF/Proof/public-inflate-header.leanProof↗public-inflate-init.leanZlibF/Proof/public-inflate-init.leanProof↗public-inflate-mark.leanZlibF/Proof/public-inflate-mark.leanProof↗public-inflate-prime.leanZlibF/Proof/public-inflate-prime.leanProof↗public-inflate-reset-keep.leanZlibF/Proof/public-inflate-reset-keep.leanProof↗public-inflate-reset.leanZlibF/Proof/public-inflate-reset.leanProof↗public-inflate-reset2.leanZlibF/Proof/public-inflate-reset2.leanProof↗public-inflate-setdict.leanZlibF/Proof/public-inflate-setdict.leanProof↗public-inflate-small-queries.leanZlibF/Proof/public-inflate-small-queries.leanProof↗public-zerror.leanZlibF/Proof/public-zerror.leanProof↗public-zlib-compile-flags.leanZlibF/Proof/public-zlib-compile-flags.leanProof↗public-zlib-version.leanZlibF/Proof/public-zlib-version.leanProof↗trees.c.align.leanZlibF/Proof/trees.c.align.leanProof↗trees.c.arrays.leanZlibF/Proof/trees.c.arrays.leanProof↗trees.c.bits.leanZlibF/Proof/trees.c.bits.leanProof↗trees.c.bl-support.leanZlibF/Proof/trees.c.bl-support.leanProof↗trees.c.bl-tree.leanZlibF/Proof/trees.c.bl-tree.leanProof↗trees.c.block.leanZlibF/Proof/trees.c.block.leanProof↗trees.c.build.complete.leanZlibF/Proof/trees.c.build.complete.leanProof↗trees.c.build.emit.leanZlibF/Proof/trees.c.build.emit.leanProof↗trees.c.build.force.leanZlibF/Proof/trees.c.build.force.leanProof↗trees.c.build.forest.leanZlibF/Proof/trees.c.build.forest.leanProof↗trees.c.build.format.leanZlibF/Proof/trees.c.build.format.leanProof↗trees.c.build.frame.leanZlibF/Proof/trees.c.build.frame.leanProof↗trees.c.build.heapify.leanZlibF/Proof/trees.c.build.heapify.leanProof↗trees.c.build.leaves.leanZlibF/Proof/trees.c.build.leaves.leanProof↗trees.c.build.lengths.leanZlibF/Proof/trees.c.build.lengths.leanProof↗trees.c.build.merge.leanZlibF/Proof/trees.c.build.merge.leanProof↗trees.c.build.order.leanZlibF/Proof/trees.c.build.order.leanProof↗trees.c.build.scan.leanZlibF/Proof/trees.c.build.scan.leanProof↗trees.c.build.static.leanZlibF/Proof/trees.c.build.static.leanProof↗trees.c.build.support.leanZlibF/Proof/trees.c.build.support.leanProof↗trees.c.build.tail.leanZlibF/Proof/trees.c.build.tail.leanProof↗trees.c.codes.leanZlibF/Proof/trees.c.codes.leanProof↗trees.c.emit-state.leanZlibF/Proof/trees.c.emit-state.leanProof↗trees.c.emit.leanZlibF/Proof/trees.c.emit.leanProof↗trees.c.heap.base.leanZlibF/Proof/trees.c.heap.base.leanProof↗trees.c.heap.gbclk.leanZlibF/Proof/trees.c.heap.gbclk.leanProof↗trees.c.heap.gbdef.leanZlibF/Proof/trees.c.heap.gbdef.leanProof↗trees.c.heap.gbfix.leanZlibF/Proof/trees.c.heap.gbfix.leanProof↗trees.c.heap.gbmath.leanZlibF/Proof/trees.c.heap.gbmath.leanProof↗trees.c.heap.gbp1.leanZlibF/Proof/trees.c.heap.gbp1.leanProof↗trees.c.heap.gbre.leanZlibF/Proof/trees.c.heap.gbre.leanProof↗trees.c.heap.gbsym.leanZlibF/Proof/trees.c.heap.gbsym.leanProof↗trees.c.heap.gbtop.leanZlibF/Proof/trees.c.heap.gbtop.leanProof↗trees.c.heap.gbtree.leanZlibF/Proof/trees.c.heap.gbtree.leanProof↗trees.c.heap.ord.leanZlibF/Proof/trees.c.heap.ord.leanProof↗trees.c.heap.pq.leanZlibF/Proof/trees.c.heap.pq.leanProof↗trees.c.heap.pqrun.leanZlibF/Proof/trees.c.heap.pqrun.leanProof↗trees.c.inv.leanZlibF/Proof/trees.c.inv.leanProof↗trees.c.monad.leanZlibF/Proof/trees.c.monad.leanProof↗trees.c.reverse.leanZlibF/Proof/trees.c.reverse.leanProof↗trees.c.runs.leanZlibF/Proof/trees.c.runs.leanProof↗trees.c.scan-tree.leanZlibF/Proof/trees.c.scan-tree.leanProof↗trees.c.send-support.leanZlibF/Proof/trees.c.send-support.leanProof↗trees.c.send-tree.leanZlibF/Proof/trees.c.send-tree.leanProof↗trees.c.tally-support.leanZlibF/Proof/trees.c.tally-support.leanProof↗trees.c.tally.leanZlibF/Proof/trees.c.tally.leanProof↗zutil.c.leanZlibF/Proof/zutil.c.leanProof↗Address.leanZlibF/Runtime/Address.leanRuntime↗Alloc.leanZlibF/Runtime/Alloc.leanRuntime↗Libc.leanZlibF/Runtime/Libc.leanRuntime↗LibcTables.leanZlibF/Runtime/LibcTables.leanRuntime↗Monad.leanZlibF/Runtime/Monad.leanRuntime↗Ptr.leanZlibF/Runtime/Ptr.leanRuntime↗Schema.leanZlibF/Runtime/Schema.leanRuntime↗Space.leanZlibF/Runtime/Space.leanRuntime↗Tables.leanZlibF/Runtime/Tables.leanRuntime↗Basic.leanZlibF/Spec/Api/Basic.leanSpec↗Compress.leanZlibF/Spec/Api/Compress.leanSpec↗Concrete.leanZlibF/Spec/Api/Concrete.leanSpec↗Deflate.leanZlibF/Spec/Api/Deflate.leanSpec↗Examples.leanZlibF/Spec/Api/Examples.leanSpec↗Goals.leanZlibF/Spec/Api/Goals.leanSpec↗Gz.leanZlibF/Spec/Api/Gz.leanSpec↗Header.leanZlibF/Spec/Api/Header.leanSpec↗Iface.leanZlibF/Spec/Api/Iface.leanSpec↗Inflate.leanZlibF/Spec/Api/Inflate.leanSpec↗Run.leanZlibF/Spec/Api/Run.leanSpec↗Api.leanZlibF/Spec/Api.leanSpec↗ByteAddress.leanZlibF/Spec/ByteAddress.leanSpec↗Crc32ByteViews.leanZlibF/Spec/Crc32ByteViews.leanSpec↗Bits.leanZlibF/Spec/Format/Bits.leanSpec↗Checksum.leanZlibF/Spec/Format/Checksum.leanSpec↗Deflate.leanZlibF/Spec/Format/Deflate.leanSpec↗Examples.leanZlibF/Spec/Format/Examples.leanSpec↗Huffman.leanZlibF/Spec/Format/Huffman.leanSpec↗Token.leanZlibF/Spec/Format/Token.leanSpec↗Wrapper.leanZlibF/Spec/Format/Wrapper.leanSpec↗Format.leanZlibF/Spec/Format.leanSpec↗InflateDecodeTableFrame.leanZlibF/Spec/InflateDecodeTableFrame.leanSpec↗InflateDecodeTableInvariant.leanZlibF/Spec/InflateDecodeTableInvariant.leanSpec↗InflateDecodeTableRejection.leanZlibF/Spec/InflateDecodeTableRejection.leanSpec↗InflateDecodeTableSemantics.leanZlibF/Spec/InflateDecodeTableSemantics.leanSpec↗InflateDecodeTableShort.leanZlibF/Spec/InflateDecodeTableShort.leanSpec↗InflateDecodeTableSoundness.leanZlibF/Spec/InflateDecodeTableSoundness.leanSpec↗InflateDecodeTableStability.leanZlibF/Spec/InflateDecodeTableStability.leanSpec↗InflateFast.leanZlibF/Spec/InflateFast.leanSpec↗InflateFastBodyOrigin.leanZlibF/Spec/InflateFastBodyOrigin.leanSpec↗InflateFastBodyToken.leanZlibF/Spec/InflateFastBodyToken.leanSpec↗InflateFastCallOrigin.leanZlibF/Spec/InflateFastCallOrigin.leanSpec↗InflateFastDistanceOrigin.leanZlibF/Spec/InflateFastDistanceOrigin.leanSpec↗InflateFastDistanceResult.leanZlibF/Spec/InflateFastDistanceResult.leanSpec↗InflateFastDistanceSemantics.leanZlibF/Spec/InflateFastDistanceSemantics.leanSpec↗InflateFastLengthSemantics.leanZlibF/Spec/InflateFastLengthSemantics.leanSpec↗InflateFastLengthTrace.leanZlibF/Spec/InflateFastLengthTrace.leanSpec↗InflateFastMatchHistory.leanZlibF/Spec/InflateFastMatchHistory.leanSpec↗InflateFastOrigin.leanZlibF/Spec/InflateFastOrigin.leanSpec↗InflateFastPlatform.leanZlibF/Spec/InflateFastPlatform.leanSpec↗InflateFastTableFlags.leanZlibF/Spec/InflateFastTableFlags.leanSpec↗InflateRootTable.leanZlibF/Spec/InflateRootTable.leanSpec↗InflateSubtable.leanZlibF/Spec/InflateSubtable.leanSpec↗InflateTableContent.leanZlibF/Spec/InflateTableContent.leanSpec↗InflateTableExtent.leanZlibF/Spec/InflateTableExtent.leanSpec↗InflateTableSafety.leanZlibF/Spec/InflateTableSafety.leanSpec↗PlatformMemory.leanZlibF/Spec/PlatformMemory.leanSpec↗Back.leanZlibF/Spec/Public/Back.leanSpec↗Calls.leanZlibF/Spec/Public/Calls.leanSpec↗Checksums.leanZlibF/Spec/Public/Checksums.leanSpec↗Copy.leanZlibF/Spec/Public/Copy.leanSpec↗Domains.leanZlibF/Spec/Public/Domains.leanSpec↗GzClose.leanZlibF/Spec/Public/GzClose.leanSpec↗GzControl.leanZlibF/Spec/Public/GzControl.leanSpec↗GzOpen.leanZlibF/Spec/Public/GzOpen.leanSpec↗GzRead.leanZlibF/Spec/Public/GzRead.leanSpec↗GzState.leanZlibF/Spec/Public/GzState.leanSpec↗GzTrace.leanZlibF/Spec/Public/GzTrace.leanSpec↗GzWrite.leanZlibF/Spec/Public/GzWrite.leanSpec↗History.leanZlibF/Spec/Public/History.leanSpec↗Initialisation.leanZlibF/Spec/Public/Initialisation.leanSpec↗Lifecycle.leanZlibF/Spec/Public/Lifecycle.leanSpec↗Memory.leanZlibF/Spec/Public/Memory.leanSpec↗Queries.leanZlibF/Spec/Public/Queries.leanSpec↗Sequences.leanZlibF/Spec/Public/Sequences.leanSpec↗StreamQueries.leanZlibF/Spec/Public/StreamQueries.leanSpec↗Streams.leanZlibF/Spec/Public/Streams.leanSpec↗Utilities.leanZlibF/Spec/Public/Utilities.leanSpec↗adler32.c.leanZlibF/Zlib/adler32.c.leanZlib↗compress.c.leanZlibF/Zlib/compress.c.leanZlib↗crc32.c.leanZlibF/Zlib/crc32.c.leanZlib↗crc32.h.leanZlibF/Zlib/crc32.h.leanZlib↗deflate.c.leanZlibF/Zlib/deflate.c.leanZlib↗deflate_base.c.leanZlibF/Zlib/deflate_base.c.leanZlib↗deflate_strategies.c.leanZlibF/Zlib/deflate_strategies.c.leanZlib↗gzclose.c.leanZlibF/Zlib/gzclose.c.leanZlib↗gzfs.leanZlibF/Zlib/gzfs.leanZlib↗gzguts.h.leanZlibF/Zlib/gzguts.h.leanZlib↗gzlib.c.leanZlibF/Zlib/gzlib.c.leanZlib↗gzread.c.leanZlibF/Zlib/gzread.c.leanZlib↗gzwrite.c.leanZlibF/Zlib/gzwrite.c.leanZlib↗infback.c.leanZlibF/Zlib/infback.c.leanZlib↗inffast.c.leanZlibF/Zlib/inffast.c.leanZlib↗inffixed.h.leanZlibF/Zlib/inffixed.h.leanZlib↗inflate.c.leanZlibF/Zlib/inflate.c.leanZlib↗inftrees.c.leanZlibF/Zlib/inftrees.c.leanZlib↗trees.c.leanZlibF/Zlib/trees.c.leanZlib↗uncompr.c.leanZlibF/Zlib/uncompr.c.leanZlib↗zutil.c.leanZlibF/Zlib/zutil.c.leanZlib↗ZlibF.leanZlibF.leanRoot↗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↗No matching modules.