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 fixpoint::*;

pub use init::*;

pub use int::*;

pub use io::*;

pub use nat::*;

pub use primitive::*;

pub use sarray::*;

pub use string::*;

pub use task::*;

pub use thunk::*;

Modules

Closures

Constructor objects

Debugging helper functions

External objects

Fixpoint

Utilities for initializing Lean’s runtime

Integers

IO Helper functions

Natural numbers

Primitive operations

Array of scalars

Strings

Tasks

Thunks

Structs

IncompleteArrayField

lean_array_object

Array arrays

lean_closure_object

lean_ctor_object

lean_external_class

lean_external_object

Lean object header.

lean_ref_object

lean_sarray_object

Scalar arrays

lean_string_object

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

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

LeanScalarArray

LeanStructArray

Functions

c_int_load ^⚠

lean_alloc_ctor_memory ^⚠

lean_alloc_object ^⚠

lean_alloc_small ^⚠

lean_alloc_small_object ^⚠

Box a usize into a lean_object

lean_dealloc ^⚠

Just free memory

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

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

lean_is_mpz ^⚠

lean_is_mt ^⚠

Whether an object is multi-threaded

lean_is_persistent ^⚠

lean_is_ref ^⚠

lean_is_sarray ^⚠

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

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 Definitions

Borrowed object argument

Borrowed object result

lean_external_finalize_proc

lean_external_foreach_proc

Standard object argument

Standard object result

lean_task_object

Unique (aka non shared) object argument