Crate lean_sys

Source

Expand description

Rust bindings to Lean 4’s C API

Functions and comments manually translated from those in the lean.h header provided with Lean 4

Re-exports§

pub use array::*;
pub use closure::*;
pub use constructor::*;
pub use dbg::*;
pub use external::*;
pub use init::*;
pub use int::*;
pub use io::*;
pub use libuv::*;
pub use nat::*;
pub use primitive::*;
pub use sarray::*;
pub use share_common::*;
pub use string::*;
pub use task::*;
pub use thread::*;
pub use thunk::*;

Modules§

alloc
array
closure: Closures
constructor: Constructor objects
dbg: Debugging helper functions
external: External objects
init: Utilities for initializing Lean’s runtime
int: Integers
io: IO Helper functions
libuv
nat: Natural numbers
panic
primitive: Primitive operations
sarray: Array of scalars
share_common
string: Strings
task: Tasks
thread: Utilities for initializing Lean threads
thunk: Thunks

Structs§

IncompleteArrayField
lean_array_object: Array arrays
lean_closure_object
lean_ctor_object
lean_external_class
lean_external_object
lean_object: Lean object header.
lean_promise_object
lean_ref_object
lean_sarray_object: Scalar arrays
lean_string_object
lean_task_imp: Data required for executing a Lean task. It is released as soon as the task terminates even if the task object itself is still referenced.
lean_task_object: Object of type Task _. The lifetime of a lean_task object can be represented as a state machine with atomic state transitions.
lean_thunk_object

Constants§

Functions§

c_int_load^⚠
layout_compat
lean_align
lean_alloc_ctor_memory^⚠
lean_alloc_object^⚠
lean_alloc_small^⚠
lean_alloc_small_object^⚠
lean_box: Box a usize into a lean_object
lean_dec^⚠
lean_dec_ref^⚠
lean_dec_ref_cold^⚠
lean_free_object^⚠
lean_free_small^⚠
lean_free_small_object^⚠
lean_get_rc_mt_addr^⚠
lean_get_slot_idx
lean_has_rc^⚠: Whether an object is reference counted
lean_inc^⚠
lean_inc_heartbeat^⚠
lean_inc_n^⚠
lean_inc_ref^⚠
lean_inc_ref_n^⚠
lean_internal_panic^⚠
lean_internal_panic_out_of_memory^⚠
lean_internal_panic_rc_overflow^⚠
lean_internal_panic_unreachable^⚠
lean_is_array^⚠
lean_is_big_object_tag
lean_is_closure^⚠
lean_is_ctor^⚠
lean_is_exclusive^⚠
lean_is_exclusive_obj^⚠
lean_is_external^⚠
lean_is_mpz^⚠
lean_is_mt^⚠: Whether an object is multi-threaded
lean_is_persistent^⚠
lean_is_promise^⚠
lean_is_ref^⚠
lean_is_sarray^⚠
lean_is_scalar: Whether this lean object is a scalar
lean_is_shared^⚠
lean_is_st^⚠: Whether an object is single-threaded
lean_is_string^⚠
lean_is_task^⚠
lean_is_thunk^⚠
lean_mark_mt^⚠
lean_mark_persistent^⚠
lean_obj_tag^⚠
lean_object_byte_size^⚠: The object size may be slightly bigger for constructor objects. The runtime does not track the size of the scalar size area. All constructor objects are “small”, and allocated into pages. We retrieve their size by accessing the page header. The size of small objects is a multiple of LEAN_OBJECT_SIZE_DELTA
lean_object_data_byte_size^⚠: Returns the size of the salient part of an object’s storage, i.e. the parts that contribute to the value representation; padding or unused capacity is excluded. Operations that read from an object’s storage must only access these parts, since the non-salient parts may not be initialized.
lean_panic^⚠
lean_panic_fn^⚠
lean_ptr_other^⚠
lean_ptr_tag^⚠
lean_set_exit_on_panic^⚠
lean_set_non_heap_header^⚠: Remark: we don’t need a reference counter for objects that are not stored in the heap. Thus, we use the area to store the object size for small objects.
lean_set_non_heap_header_for_big^⚠: lean_set_non_heap_header for (potentially) big objects such as arrays and strings.
lean_set_panic_messages^⚠: Enable/disable panic messages
lean_set_st_header^⚠
lean_small_mem_size^⚠
lean_small_object_size^⚠
lean_to_array^⚠
lean_to_closure^⚠
lean_to_ctor^⚠
lean_to_external^⚠
lean_to_promise^⚠
lean_to_ref^⚠
lean_to_sarray^⚠
lean_to_string^⚠
lean_to_task^⚠
lean_to_thunk^⚠
lean_unbox: Unbox a lean_object into a usize
relaxed_rc_load^⚠: Perform a relaxed load of the reference counter of o, which must be a pointer into a valid lean_object

Type Aliases§

b_lean_obj_arg: Borrowed object argument
b_lean_obj_res: Borrowed object result
lean_external_finalize_proc
lean_external_foreach_proc
lean_obj_arg: Standard object argument
lean_obj_res: Standard object result
u_lean_obj_arg: Unique (aka non shared) object argument

Crate lean_sys

Crate lean_sys Copy item path

Re-exports§

Modules§

Structs§

Constants§

Functions§

Type Aliases§

Crate lean_sys