From 4fa1a496b324573fec011f1e565c1cea81574ae9 Mon Sep 17 00:00:00 2001 From: David Renshaw Date: Fri, 7 Oct 2022 11:43:46 -0400 Subject: [PATCH] doc: Lean USize maps to C++ size_t, not usize_t usize_t is not a standard C++ type. See src/include/lean/lean.h for translations between USize and size_t. --- doc/dev/ffi.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/dev/ffi.md b/doc/dev/ffi.md index 0b55f5c4b2..3e92abd2e4 100644 --- a/doc/dev/ffi.md +++ b/doc/dev/ffi.md @@ -32,7 +32,7 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se ### Translating Types from Lean to C -* The integer types `UInt8`, ..., `UInt64`, `USize` are represented by the C types `uint8_t`, ..., `uint64_t`, `usize_t`, respectively +* The integer types `UInt8`, ..., `UInt64`, `USize` are represented by the C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively * `Char` is represented by `uint32_t` * `Float` is represented by `double` * An *enum* inductive type of at least 2 and at most 2^32 constructors, each of which with no parameters, is represented by the first type of `uint8_t`, `uint16_t`, `uint32_t` that is sufficient to represent all constructor indices.