L4YAML

5.5. Adding FFI Bindings🔗

To expose a new Lean function via FFI:

  1. Add @[export l4yaml_function_name] to the Lean definition

  2. Declare the corresponding C prototype in ffi/l4yaml.h

  3. Add any necessary shim code in ffi/l4yaml_shim.c

  4. Update the Python/Rust wrappers as needed

  5. Add tests at each layer

The @[export] attribute instructs the Lean compiler to generate a C-callable symbol with the specified name.