参考文档 / ZLIB × LEAN

public-zlib-version.lean

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

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

1import ZlibF.Spec.Public.Queries
2
3namespace ZlibF.Spec.Public.Proofs
4open C
5
6set_option maxRecDepth 100000 in
7/-- `const char *zlibVersion(void)`: return the read-only pinned version string. -/
8theorem zlibVersion : Goal.zlibVersion := by
9  intro h
10  have hm : ZLIB_VERSION ∈ strTable := by
11    rw [Array.mem_def]
12    decide +kernel
13  obtain ⟨i, hr, hi⟩ := strLitRef_of_mem (h := h) hm
14  refine ⟨.ref (.str i) 0, ?_, i, rfl, ?_, rfl⟩
15  · exact hr
16  · simp [hi, strBytes]
17
18#print axioms zlibVersion
19end ZlibF.Spec.Public.Proofs