参考文档 / ZLIB × LEAN

public-zlib-compile-flags.lean

此页源文件快照 · c4ff364e7bd90a05 · 对应提交的原文 ↗

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

1import ZlibF.Spec.Public.Queries
2
3namespace ZlibF.Spec.Public.Proofs
4
5/-- `uLong zlibCompileFlags(void)`: the default LP64 flags, with the heap unchanged. -/
6theorem zlibCompileFlags : Goal.zlibCompileFlags := by
7  intro h
8  rfl
9
10#print axioms zlibCompileFlags
11end ZlibF.Spec.Public.Proofs