Crate lean_sys

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_ref_object

lean_sarray_object

Scalar arrays

lean_string_object

lean_task

Object of type Task _. The lifetime of a lean_task object can be represented as a state machine with atomic state transitions.

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_thunk_object

Constants

LEAN_CLOSURE_MAX_ARGS

LEAN_MAX_CTOR_FIELDS

LEAN_MAX_CTOR_SCALARS_SIZE

LEAN_MAX_SMALL_OBJECT_SIZE

LEAN_OBJECT_SIZE_DELTA

LEAN_SMALL_ALLOCATOR

LeanArray

LeanClosure

LeanExternal

LeanMPZ

LeanMaxCtorTag

LeanRef

LeanReserved

LeanScalarArray

LeanString

LeanStructArray

LeanTask

LeanThunk

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_cold^⚠

lean_inc_ref_n^⚠

lean_inc_ref_n_cold^⚠

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_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_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_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

lean_task_object

u_lean_obj_arg

Unique (aka non shared) object argument