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 nat::*;
• pub use primitive::*;
• pub use sarray::*;
• pub use string::*;
• pub use task::*;
• 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
• nat
  Natural numbers
• panic
• primitive
  Primitive operations
• sarray
  Array of scalars
• string
  Strings
• task
  Tasks
• 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_dealloc^⚠
  Just free memory
• 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_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_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