REFERENCE / ZLIB × LEAN

public-zlib-compile-flags.lean

Source snapshot · c4ff364e7bd90a05 · Source at the matching commit ↗

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

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