Liking cljdoc? Tell your friends :D
Clojure only.

lean-clj.runtime

Runtime for Clojure code generated from Lean IR.

Functions named lean_* implement the C symbols of Lean's @[extern] declarations, so generated code calls lean-clj.runtime/<C symbol>. Value representation:

  • Nat / Int: Long, or clojure.lang.BigInt when it does not fit
  • UInt8..UInt32, Char, Bool, enumerations: Long
  • UInt64 / USize: Long holding the 64-bit pattern
  • Float: Double
  • String: java.lang.String (positions are UTF-8 byte offsets)
  • Array: persistent vector
  • nullary constructors: Long (the constructor index)
  • other constructors: Ctor
  • closures: Closure
Runtime for Clojure code generated from Lean IR.

Functions named `lean_*` implement the C symbols of Lean's `@[extern]`
declarations, so generated code calls `lean-clj.runtime/<C symbol>`.
Value representation:

- `Nat` / `Int`: `Long`, or `clojure.lang.BigInt` when it does not fit
- `UInt8`..`UInt32`, `Char`, `Bool`, enumerations: `Long`
- `UInt64` / `USize`: `Long` holding the 64-bit pattern
- `Float`: `Double`
- `String`: `java.lang.String` (positions are UTF-8 byte offsets)
- `Array`: persistent vector
- nullary constructors: `Long` (the constructor index)
- other constructors: `Ctor`
- closures: `Closure`
raw docstring

applyclj

(apply f & args)
source

apply-vclj

(apply-v f args)
source

ceilclj

(ceil a)
source

check-symbols!clj

(check-symbols! syms)
source

closureclj

(closure f arity args)
source

cosclj

(cos a)
source

ctorclj

(ctor tag nobjs ssize & objs)
source

expclj

(exp a)
source

floorclj

(floor a)
source

from-cljclj

(from-clj d v)
source

lean_array_fgetclj

(lean_array_fget a i)
source

lean_array_fget_borrowedclj

(lean_array_fget_borrowed a i)
source

lean_array_fsetclj

(lean_array_fset a i v)
source

lean_array_fswapclj

(lean_array_fswap a i j)
source

lean_array_getclj

(lean_array_get dflt a i)
source

lean_array_get_borrowedclj

(lean_array_get_borrowed dflt a i)
source

lean_array_get_panicclj

(lean_array_get_panic dflt)
source

lean_array_get_sizeclj

(lean_array_get_size a)
source

lean_array_mkclj

(lean_array_mk l)
source

lean_array_popclj

(lean_array_pop a)
source

lean_array_propagate_markclj

(lean_array_propagate_mark _ ys)
source

lean_array_pushclj

(lean_array_push a v)
source

lean_array_setclj

(lean_array_set a i v)
source

lean_array_sizeclj

(lean_array_size a)
source

lean_array_swapclj

(lean_array_swap a i j)
source

lean_array_to_listclj

(lean_array_to_list a)
source

lean_array_ugetclj

(lean_array_uget a i)
source

lean_array_uget_borrowedclj

(lean_array_uget_borrowed a i)
source

lean_array_usetclj

(lean_array_uset a i v)
source

lean_float_addclj

(lean_float_add a b)
source

lean_float_beqclj

(lean_float_beq a b)
source

lean_float_decLeclj

(lean_float_decLe a b)
source

lean_float_decLtclj

(lean_float_decLt a b)
source

lean_float_divclj

(lean_float_div a b)
source

lean_float_mulclj

(lean_float_mul a b)
source

lean_float_negateclj

(lean_float_negate a)
source

lean_float_of_bitsclj

(lean_float_of_bits a)
source

lean_float_of_natclj

(lean_float_of_nat a)
source

lean_float_of_scientificclj

(lean_float_of_scientific m s e)
source

lean_float_subclj

(lean_float_sub a b)
source

lean_float_to_bitsclj

(lean_float_to_bits a)
source

lean_float_to_stringclj

(lean_float_to_string a)
source

lean_float_to_uint64clj

(lean_float_to_uint64 a)
source

lean_int_addclj

(lean_int_add a b)
source

lean_int_dec_eqclj

(lean_int_dec_eq a b)
source

lean_int_dec_leclj

(lean_int_dec_le a b)
source

lean_int_dec_ltclj

(lean_int_dec_lt a b)
source

lean_int_dec_nonnegclj

(lean_int_dec_nonneg a)
source

lean_int_divclj

(lean_int_div a b)
source

lean_int_edivclj

(lean_int_ediv a b)
source

lean_int_emodclj

(lean_int_emod a b)
source

lean_int_modclj

(lean_int_mod a b)
source

lean_int_mulclj

(lean_int_mul a b)
source

lean_int_negclj

(lean_int_neg a)
source

lean_int_neg_succ_of_natclj

(lean_int_neg_succ_of_nat a)
source

lean_int_subclj

(lean_int_sub a b)
source

lean_int_to_intclj

(lean_int_to_int a)
source

lean_int_to_natclj

(lean_int_to_nat a)
source

lean_mk_arrayclj

(lean_mk_array n v)
source

lean_mk_empty_array_with_capacityclj

(lean_mk_empty_array_with_capacity _)
source

lean_nat_absclj

(lean_nat_abs a)
source

lean_nat_addclj

(lean_nat_add a b)
source

lean_nat_dec_eqclj

(lean_nat_dec_eq a b)
source

lean_nat_dec_leclj

(lean_nat_dec_le a b)
source

lean_nat_dec_ltclj

(lean_nat_dec_lt a b)
source

lean_nat_divclj

(lean_nat_div a b)
source

lean_nat_gcdclj

(lean_nat_gcd a b)
source

lean_nat_landclj

(lean_nat_land a b)
source

lean_nat_lcmclj

(lean_nat_lcm a b)
source

lean_nat_log2clj

(lean_nat_log2 a)
source

lean_nat_lorclj

(lean_nat_lor a b)
source

lean_nat_lxorclj

(lean_nat_lxor a b)
source

lean_nat_modclj

(lean_nat_mod a b)
source

lean_nat_mulclj

(lean_nat_mul a b)
source

lean_nat_powclj

(lean_nat_pow a b)
source

lean_nat_predclj

(lean_nat_pred a)
source

lean_nat_shiftlclj

(lean_nat_shiftl a b)
source

lean_nat_shiftrclj

(lean_nat_shiftr a b)
source

lean_nat_subclj

(lean_nat_sub a b)
source

lean_nat_succclj

(lean_nat_succ a)
source

lean_nat_to_intclj

(lean_nat_to_int a)
source

lean_panic_fnclj

(lean_panic_fn dflt msg)
source

lean_panic_fn_borrowedclj

(lean_panic_fn_borrowed dflt msg)
source

lean_string_anyclj

(lean_string_any s p)
source

lean_string_appendclj

(lean_string_append a b)
source

lean_string_dataclj

(lean_string_data s)
source

lean_string_dec_eqclj

(lean_string_dec_eq a b)
source

lean_string_dec_ltclj

(lean_string_dec_lt a b)
source

lean_string_foldlclj

(lean_string_foldl f init s)
source

lean_string_get_byte_fastclj

(lean_string_get_byte_fast s i)
source

lean_string_hashclj

(lean_string_hash s)
source

lean_string_isemptyclj

(lean_string_isempty s)
source

lean_string_isprefixofclj

(lean_string_isprefixof p s)
source

lean_string_lengthclj

(lean_string_length s)
source

lean_string_memcmpclj

(lean_string_memcmp a b ls rs len)
source

lean_string_mkclj

(lean_string_mk cs)
source

lean_string_of_usizeclj

(lean_string_of_usize a)
source

lean_string_offsetofposclj

(lean_string_offsetofpos s pos)
source

lean_string_posofclj

(lean_string_posof s c)
source

lean_string_pushclj

(lean_string_push s c)
source

lean_string_pushnclj

(lean_string_pushn s c n)
source

lean_string_utf8_at_endclj

(lean_string_utf8_at_end s i)
source

lean_string_utf8_byte_sizeclj

(lean_string_utf8_byte_size s)
source

lean_string_utf8_extractclj

(lean_string_utf8_extract s b e)
source

lean_string_utf8_extract_fastclj

(lean_string_utf8_extract_fast s b e)
source

lean_string_utf8_getclj

(lean_string_utf8_get s i)
source

lean_string_utf8_get_fastclj

(lean_string_utf8_get_fast s i)
source

lean_string_utf8_nextclj

(lean_string_utf8_next s i)
source

lean_string_utf8_next_fastclj

(lean_string_utf8_next_fast s i)
source

lean_string_utf8_prevclj

(lean_string_utf8_prev s i)
source

lean_string_utf8_setclj

(lean_string_utf8_set s i c)
source

lean_system_platform_nbitsclj

(lean_system_platform_nbits _)
source

lean_uint16_addclj

(lean_uint16_add a__1896__auto__ b__1897__auto__)
source

lean_uint16_complementclj

(lean_uint16_complement a__1896__auto__)
source

lean_uint16_dec_eqclj

(lean_uint16_dec_eq a__1896__auto__ b__1897__auto__)
source

lean_uint16_dec_leclj

(lean_uint16_dec_le a__1896__auto__ b__1897__auto__)
source

lean_uint16_dec_ltclj

(lean_uint16_dec_lt a__1896__auto__ b__1897__auto__)
source

lean_uint16_divclj

(lean_uint16_div a__1896__auto__ b__1897__auto__)
source

lean_uint16_landclj

(lean_uint16_land a__1896__auto__ b__1897__auto__)
source

lean_uint16_lorclj

(lean_uint16_lor a__1896__auto__ b__1897__auto__)
source

lean_uint16_modclj

(lean_uint16_mod a__1896__auto__ b__1897__auto__)
source

lean_uint16_mulclj

(lean_uint16_mul a__1896__auto__ b__1897__auto__)
source

lean_uint16_negclj

(lean_uint16_neg a__1896__auto__)
source

lean_uint16_of_natclj

(lean_uint16_of_nat a__1896__auto__)
source

lean_uint16_shift_leftclj

(lean_uint16_shift_left a__1896__auto__ b__1897__auto__)
source

lean_uint16_shift_rightclj

(lean_uint16_shift_right a__1896__auto__ b__1897__auto__)
source

lean_uint16_subclj

(lean_uint16_sub a__1896__auto__ b__1897__auto__)
source

lean_uint16_to_floatclj

(lean_uint16_to_float a__1896__auto__)
source

lean_uint16_to_natclj

(lean_uint16_to_nat a__1896__auto__)
source

lean_uint16_to_uint16clj

(lean_uint16_to_uint16 a__1896__auto__)
source

lean_uint16_to_uint32clj

(lean_uint16_to_uint32 a__1896__auto__)
source

lean_uint16_to_uint64clj

(lean_uint16_to_uint64 a__1896__auto__)
source

lean_uint16_to_uint8clj

(lean_uint16_to_uint8 a__1896__auto__)
source

lean_uint16_to_usizeclj

(lean_uint16_to_usize a__1896__auto__)
source

lean_uint16_xorclj

(lean_uint16_xor a__1896__auto__ b__1897__auto__)
source

lean_uint32_addclj

(lean_uint32_add a__1896__auto__ b__1897__auto__)
source

lean_uint32_complementclj

(lean_uint32_complement a__1896__auto__)
source

lean_uint32_dec_eqclj

(lean_uint32_dec_eq a__1896__auto__ b__1897__auto__)
source

lean_uint32_dec_leclj

(lean_uint32_dec_le a__1896__auto__ b__1897__auto__)
source

lean_uint32_dec_ltclj

(lean_uint32_dec_lt a__1896__auto__ b__1897__auto__)
source

lean_uint32_divclj

(lean_uint32_div a__1896__auto__ b__1897__auto__)
source

lean_uint32_landclj

(lean_uint32_land a__1896__auto__ b__1897__auto__)
source

lean_uint32_lorclj

(lean_uint32_lor a__1896__auto__ b__1897__auto__)
source

lean_uint32_modclj

(lean_uint32_mod a__1896__auto__ b__1897__auto__)
source

lean_uint32_mulclj

(lean_uint32_mul a__1896__auto__ b__1897__auto__)
source

lean_uint32_negclj

(lean_uint32_neg a__1896__auto__)
source

lean_uint32_of_natclj

(lean_uint32_of_nat a__1896__auto__)
source

lean_uint32_of_nat_mkclj

(lean_uint32_of_nat_mk a)
source

lean_uint32_shift_leftclj

(lean_uint32_shift_left a__1896__auto__ b__1897__auto__)
source

lean_uint32_shift_rightclj

(lean_uint32_shift_right a__1896__auto__ b__1897__auto__)
source

lean_uint32_subclj

(lean_uint32_sub a__1896__auto__ b__1897__auto__)
source

lean_uint32_to_floatclj

(lean_uint32_to_float a__1896__auto__)
source

lean_uint32_to_natclj

(lean_uint32_to_nat a__1896__auto__)
source

lean_uint32_to_uint16clj

(lean_uint32_to_uint16 a__1896__auto__)
source

lean_uint32_to_uint32clj

(lean_uint32_to_uint32 a__1896__auto__)
source

lean_uint32_to_uint64clj

(lean_uint32_to_uint64 a__1896__auto__)
source

lean_uint32_to_uint8clj

(lean_uint32_to_uint8 a__1896__auto__)
source

lean_uint32_to_usizeclj

(lean_uint32_to_usize a__1896__auto__)
source

lean_uint32_xorclj

(lean_uint32_xor a__1896__auto__ b__1897__auto__)
source

lean_uint64_addclj

(lean_uint64_add a__1975__auto__ b__1976__auto__)
source

lean_uint64_complementclj

(lean_uint64_complement a__1975__auto__)
source

lean_uint64_dec_eqclj

(lean_uint64_dec_eq a__1975__auto__ b__1976__auto__)
source

lean_uint64_dec_leclj

(lean_uint64_dec_le a__1975__auto__ b__1976__auto__)
source

lean_uint64_dec_ltclj

(lean_uint64_dec_lt a__1975__auto__ b__1976__auto__)
source

lean_uint64_divclj

(lean_uint64_div a__1975__auto__ b__1976__auto__)
source

lean_uint64_landclj

(lean_uint64_land a__1975__auto__ b__1976__auto__)
source

lean_uint64_lorclj

(lean_uint64_lor a__1975__auto__ b__1976__auto__)
source

lean_uint64_modclj

(lean_uint64_mod a__1975__auto__ b__1976__auto__)
source

lean_uint64_mulclj

(lean_uint64_mul a__1975__auto__ b__1976__auto__)
source

lean_uint64_negclj

(lean_uint64_neg a__1975__auto__)
source

lean_uint64_of_natclj

(lean_uint64_of_nat a__1975__auto__)
source

lean_uint64_of_nat_mkclj

(lean_uint64_of_nat_mk a)
source

lean_uint64_shift_leftclj

(lean_uint64_shift_left a__1975__auto__ b__1976__auto__)
source

lean_uint64_shift_rightclj

(lean_uint64_shift_right a__1975__auto__ b__1976__auto__)
source

lean_uint64_subclj

(lean_uint64_sub a__1975__auto__ b__1976__auto__)
source

lean_uint64_to_floatclj

(lean_uint64_to_float a__1975__auto__)
source

lean_uint64_to_natclj

(lean_uint64_to_nat a__1975__auto__)
source

lean_uint64_to_uint16clj

(lean_uint64_to_uint16 a__1975__auto__)
source

lean_uint64_to_uint32clj

(lean_uint64_to_uint32 a__1975__auto__)
source

lean_uint64_to_uint64clj

(lean_uint64_to_uint64 a__1975__auto__)
source

lean_uint64_to_uint8clj

(lean_uint64_to_uint8 a__1975__auto__)
source

lean_uint64_to_usizeclj

(lean_uint64_to_usize a__1975__auto__)
source

lean_uint64_xorclj

(lean_uint64_xor a__1975__auto__ b__1976__auto__)
source

lean_uint8_addclj

(lean_uint8_add a__1896__auto__ b__1897__auto__)
source

lean_uint8_complementclj

(lean_uint8_complement a__1896__auto__)
source

lean_uint8_dec_eqclj

(lean_uint8_dec_eq a__1896__auto__ b__1897__auto__)
source

lean_uint8_dec_leclj

(lean_uint8_dec_le a__1896__auto__ b__1897__auto__)
source

lean_uint8_dec_ltclj

(lean_uint8_dec_lt a__1896__auto__ b__1897__auto__)
source

lean_uint8_divclj

(lean_uint8_div a__1896__auto__ b__1897__auto__)
source

lean_uint8_landclj

(lean_uint8_land a__1896__auto__ b__1897__auto__)
source

lean_uint8_lorclj

(lean_uint8_lor a__1896__auto__ b__1897__auto__)
source

lean_uint8_modclj

(lean_uint8_mod a__1896__auto__ b__1897__auto__)
source

lean_uint8_mulclj

(lean_uint8_mul a__1896__auto__ b__1897__auto__)
source

lean_uint8_negclj

(lean_uint8_neg a__1896__auto__)
source

lean_uint8_of_natclj

(lean_uint8_of_nat a__1896__auto__)
source

lean_uint8_shift_leftclj

(lean_uint8_shift_left a__1896__auto__ b__1897__auto__)
source

lean_uint8_shift_rightclj

(lean_uint8_shift_right a__1896__auto__ b__1897__auto__)
source

lean_uint8_subclj

(lean_uint8_sub a__1896__auto__ b__1897__auto__)
source

lean_uint8_to_floatclj

(lean_uint8_to_float a__1896__auto__)
source

lean_uint8_to_natclj

(lean_uint8_to_nat a__1896__auto__)
source

lean_uint8_to_uint16clj

(lean_uint8_to_uint16 a__1896__auto__)
source

lean_uint8_to_uint32clj

(lean_uint8_to_uint32 a__1896__auto__)
source

lean_uint8_to_uint64clj

(lean_uint8_to_uint64 a__1896__auto__)
source

lean_uint8_to_uint8clj

(lean_uint8_to_uint8 a__1896__auto__)
source

lean_uint8_to_usizeclj

(lean_uint8_to_usize a__1896__auto__)
source

lean_uint8_xorclj

(lean_uint8_xor a__1896__auto__ b__1897__auto__)
source

lean_usize_addclj

(lean_usize_add a__1975__auto__ b__1976__auto__)
source

lean_usize_complementclj

(lean_usize_complement a__1975__auto__)
source

lean_usize_dec_eqclj

(lean_usize_dec_eq a__1975__auto__ b__1976__auto__)
source

lean_usize_dec_leclj

(lean_usize_dec_le a__1975__auto__ b__1976__auto__)
source

lean_usize_dec_ltclj

(lean_usize_dec_lt a__1975__auto__ b__1976__auto__)
source

lean_usize_divclj

(lean_usize_div a__1975__auto__ b__1976__auto__)
source

lean_usize_landclj

(lean_usize_land a__1975__auto__ b__1976__auto__)
source

lean_usize_lorclj

(lean_usize_lor a__1975__auto__ b__1976__auto__)
source

lean_usize_modclj

(lean_usize_mod a__1975__auto__ b__1976__auto__)
source

lean_usize_mulclj

(lean_usize_mul a__1975__auto__ b__1976__auto__)
source

lean_usize_negclj

(lean_usize_neg a__1975__auto__)
source

lean_usize_of_natclj

(lean_usize_of_nat a)
source

lean_usize_shift_leftclj

(lean_usize_shift_left a__1975__auto__ b__1976__auto__)
source

lean_usize_shift_rightclj

(lean_usize_shift_right a__1975__auto__ b__1976__auto__)
source

lean_usize_subclj

(lean_usize_sub a__1975__auto__ b__1976__auto__)
source

lean_usize_to_floatclj

(lean_usize_to_float a__1975__auto__)
source

lean_usize_to_natclj

(lean_usize_to_nat a__1975__auto__)
source

lean_usize_to_uint16clj

(lean_usize_to_uint16 a__1975__auto__)
source

lean_usize_to_uint32clj

(lean_usize_to_uint32 a__1975__auto__)
source

lean_usize_to_uint64clj

(lean_usize_to_uint64 a__1975__auto__)
source

lean_usize_to_uint8clj

(lean_usize_to_uint8 a__1975__auto__)
source

lean_usize_to_usizeclj

(lean_usize_to_usize a__1975__auto__)
source

lean_usize_xorclj

(lean_usize_xor a__1975__auto__ b__1976__auto__)
source

logclj

(log a)
source

powclj

(pow a b)
source

projclj

(proj x i)
source

register-type!clj

(register-type! k desc)
source

restartclj

(restart & args)
source

restart-argclj

(restart-arg r i)
source

restart?clj

(restart? r)
source

roundclj

(round a)
source

set-obj!clj

(set-obj! x i v)
source

set-tag!clj

(set-tag! x t)
source

sinclj

(sin a)
source

sprojclj

(sproj x offset)
source

sqrtclj

(sqrt a)
source

sset!clj

(sset! x offset v)
source

tagclj

(tag x)
source

tail-callclj

(tail-call f & args)
source

tanclj

(tan a)
source

to-cljclj

(to-clj d v)
source

trampolineclj

(trampoline r)
source

unreachableclj

(unreachable)
source

cljdoc builds & hosts documentation for Clojure/Script libraries

Keyboard shortcuts
Ctrl+kJump to recent docs
←Move to previous article
→Move to next article
Ctrl+/Jump to the search field
Raise an issueBrowse cljdoc sourceChat on Slack
× close