gzclose.c.lean

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

1import ZlibF.Zlib.«gzread.c»
2import ZlibF.Zlib.«gzwrite.c»
3
4/-!
5# gzclose.c — faithful translation
6
7`NO_GZCOMPRESS` is undefined, so the `#ifndef NO_GZCOMPRESS` branch is live.
8-/
9
10namespace Zlib.Gzclose
11open C Zlib.GzFs Zlib.Gzguts Zlib.Gzlib
12
13/-- `int ZEXPORT gzclose(gzFile file)` -/
14def gzclose (file : GzFilePtr) : G Int32 := do
15  -- if (file == NULL) return Z_STREAM_ERROR;
16  if file.isNone then return Z_STREAM_ERROR
17  -- state = (gz_statep)file;
18  let state := castState file
19  -- return state->mode == GZ_READ ? gzclose_r(file) : gzclose_w(file);
20  if (← ldS state).mode == GZ_READ then Zlib.Gzread.gzclose_r file else Zlib.Gzwrite.gzclose_w file
21
22end Zlib.Gzclose