Alloc.lean

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

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-/