FFI

Stream: lean4

[Cole Shepherd]

How do you represent a C pointer in Lean 4 for FFI purposes?

[Tomas Skrivan]

There is no canonical way to represent a pointer in Lean 4 but I would suggest looking at for example how ByteArray is implemented.

Here is the Lean code and here is the c++ code.

However, for wrapping external objects into Lean objects it is recommended to use lean_external_object, see an example project.