FFI

ffi_data : (rec : FFI) -> Type

How this FFI describes exported datatypes

ffi_fn : (rec : FFI) -> Type

The type used to specify the names of foreign functions in this FFI

ffi_types : (rec : FFI) -> Type -> Type

A family describing which types are available in the FFI

set_ffi_data : (ffi_data : Type) -> (rec : FFI) -> FFI

How this FFI describes exported datatypes

set_ffi_fn : (ffi_fn : Type) -> (rec : FFI) -> FFI

The type used to specify the names of foreign functions in this FFI

set_ffi_types : (ffi_types : Type -> Type) -> (rec : FFI) -> FFI

A family describing which types are available in the FFI