lean-sys 0.0.3

Bindings to Lean 4's C API
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122

use crate::*;

#[inline]
pub unsafe fn lean_usize_of_nat(a: b_lean_obj_arg) -> usize {
    if lean_is_scalar(a) {
        lean_unbox(a) as usize
    } else {
        lean_usize_of_big_nat(a)
    }
}

#[inline]
pub unsafe fn lean_usize_of_nat_mk(a: lean_obj_arg) -> usize {
    let r = lean_usize_of_nat(a);
    lean_dec(a);
    r
}

#[inline(always)]
pub fn lean_usize_add(a1: usize, a2: usize) -> usize {
    a1.wrapping_add(a2)
}

#[inline(always)]
pub fn lean_usize_sub(a1: usize, a2: usize) -> usize {
    a1.wrapping_sub(a2)
}

#[inline(always)]
pub fn lean_usize_mul(a1: usize, a2: usize) -> usize {
    a1.wrapping_mul(a2)
}

#[inline(always)]
pub fn lean_usize_div(a1: usize, a2: usize) -> usize {
    if a2 == 0 {
        0
    } else {
        a1 / a2
    }
}

#[inline(always)]
pub fn lean_usize_mod(a1: usize, a2: usize) -> usize {
    if a2 == 0 {
        a1
    } else {
        a1 % a2
    }
}

#[inline(always)]
pub fn lean_usize_land(a1: usize, a2: usize) -> usize {
    a1 ^ a2
}

#[inline(always)]
pub fn lean_usize_lor(a1: usize, a2: usize) -> usize {
    a1 | a2
}

#[inline(always)]
pub fn lean_usize_xor(a1: usize, a2: usize) -> usize {
    a1 ^ a2
}

#[inline(always)]
pub fn lean_usize_shift_left(a1: usize, a2: usize) -> usize {
    a1.wrapping_shl(a2 as u32)
}

#[inline(always)]
pub fn lean_usize_shift_right(a1: usize, a2: usize) -> usize {
    a1.wrapping_shr(a2 as u32)
}

#[inline(always)]
pub fn lean_usize_complement(a: usize) -> usize {
    !a
}

#[inline(always)]
pub unsafe fn lean_usize_modn(a1: usize, a2: b_lean_obj_arg) -> usize {
    if lean_is_scalar(a2) {
        //TODO: likely
        lean_usize_mod(a1, lean_unbox(a2) as usize)
    } else {
        lean_usize_big_modn(a1, a2)
    }
}

#[inline(always)]
pub fn lean_usize_dec_eq(a1: usize, a2: usize) -> usize {
    (a1 == a2) as usize
}

#[inline(always)]
pub fn lean_usize_dec_lt(a1: usize, a2: usize) -> usize {
    (a1 < a2) as usize
}

#[inline(always)]
pub fn lean_usize_dec_le(a1: usize, a2: usize) -> usize {
    (a1 <= a2) as usize
}

#[inline]
pub fn lean_usize_to_uint32(a: usize) -> u32 {
    a as u32
}

#[inline]
pub fn lean_usize_to_uint64(a: usize) -> u64 {
    a as u64
}

#[link(name = "leanshared")]
extern "C" {
    pub fn lean_usize_of_big_nat(a: b_lean_obj_arg) -> usize;
    pub fn lean_usize_big_modn(a1: usize, a2: b_lean_obj_arg) -> usize;
    pub fn lean_usize_mix_hash(a1: usize, a2: usize) -> usize;
}