Alloc.lean

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

1import ZlibF.Runtime.Libc
2
3/-!
4# Runtime: allocation (moved)
5
6`malloc`, `free` and the string literals model the C library, so they are in `Libc.lean` (with `memcpy`, `memset`,
7`strlen`). This module only imports it, so that the modules that import `ZlibF.Runtime.Alloc` keep working.
8-/