Function lean_sys::lean_is_scalar

source ·
pub fn lean_is_scalar(obj: *const lean_object) -> bool
Expand description

Whether this lean object is a scalar

Examples

unsafe { lean_initialize_runtime_module(); }
let arr = unsafe { lean_mk_empty_array() };
assert!(lean_is_scalar(lean_box(5)));
assert!(!lean_is_scalar(arr));