max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc: Lean USize maps to C++ size_t, not usize_t

Browse source 
usize_t is not a standard C++ type.

See src/include/lean/lean.h for translations between USize and size_t.
This commit is contained in:
David Renshaw 2022-10-07 11:43:46 -04:00 • committed by Sebastian Ullrich
parent d22916fdcd
commit 4fa1a496b3
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/dev/ffi.md
View file

@ -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.