lean_sys/primitive/
name.rs

1/*! Name primitives */
2use crate::*;
3
4extern "C" {
5    pub fn lean_name_eq(n1: b_lean_obj_arg, n2: b_lean_obj_arg) -> bool;
6    pub fn lean_name_hash_exported(n: lean_obj_arg) -> u64;
7}
8
9#[inline(always)]
10pub unsafe fn lean_name_hash_ptr(n: b_lean_obj_arg) -> u64 {
11    debug_assert!(!lean_is_scalar(n));
12    lean_ctor_get_uint64(n, (core::mem::size_of::<*mut lean_object>() * 2) as u32)
13}
14
15#[inline]
16pub unsafe fn lean_name_hash(n: b_lean_obj_arg) -> u64 {
17    if lean_is_scalar(n) {
18        //TODO: why?
19        1273
20    } else {
21        lean_name_hash_ptr(n)
22    }
23}
24
25#[inline]
26pub unsafe fn lean_name_hash_exported_b(n: b_lean_obj_arg) -> u64 {
27    lean_inc(n);
28    lean_name_hash_exported(n)
29}
lean_sys/primitive/name.rs

lean_sys/primitive/
name.rs
