lean_sys/primitive/
usize_.rs

1use crate::*;
2
3#[inline]
4pub unsafe fn lean_usize_of_nat(a: b_lean_obj_arg) -> usize {
5    if lean_is_scalar(a) {
6        lean_unbox(a)
7    } else {
8        lean_usize_of_big_nat(a)
9    }
10}
11
12#[inline]
13pub unsafe fn lean_usize_of_nat_mk(a: lean_obj_arg) -> usize {
14    let r = lean_usize_of_nat(a);
15    lean_dec(a);
16    r
17}
18
19#[inline(always)]
20pub fn lean_usize_add(a1: usize, a2: usize) -> usize {
21    a1.wrapping_add(a2)
22}
23
24#[inline(always)]
25pub fn lean_usize_sub(a1: usize, a2: usize) -> usize {
26    a1.wrapping_sub(a2)
27}
28
29#[inline(always)]
30pub fn lean_usize_mul(a1: usize, a2: usize) -> usize {
31    a1.wrapping_mul(a2)
32}
33
34#[inline(always)]
35pub fn lean_usize_div(a1: usize, a2: usize) -> usize {
36    if a2 == 0 {
37        0
38    } else {
39        a1 / a2
40    }
41}
42
43#[inline(always)]
44pub fn lean_usize_mod(a1: usize, a2: usize) -> usize {
45    if a2 == 0 {
46        a1
47    } else {
48        a1 % a2
49    }
50}
51
52#[inline(always)]
53pub fn lean_usize_land(a1: usize, a2: usize) -> usize {
54    a1 & a2
55}
56
57#[inline(always)]
58pub fn lean_usize_lor(a1: usize, a2: usize) -> usize {
59    a1 | a2
60}
61
62#[inline(always)]
63pub fn lean_usize_xor(a1: usize, a2: usize) -> usize {
64    a1 ^ a2
65}
66
67#[inline(always)]
68pub fn lean_usize_shift_left(a1: usize, a2: usize) -> usize {
69    a1.wrapping_shl(a2 as u32)
70}
71
72#[inline(always)]
73pub fn lean_usize_shift_right(a1: usize, a2: usize) -> usize {
74    a1.wrapping_shr(a2 as u32)
75}
76
77#[inline(always)]
78pub fn lean_usize_complement(a: usize) -> usize {
79    !a
80}
81
82#[inline(always)]
83pub fn lean_usize_neg(a: usize) -> usize {
84    0 - a
85}
86
87#[inline(always)]
88pub fn lean_usize_dec_eq(a1: usize, a2: usize) -> usize {
89    (a1 == a2) as usize
90}
91
92#[inline(always)]
93pub fn lean_usize_dec_lt(a1: usize, a2: usize) -> usize {
94    (a1 < a2) as usize
95}
96
97#[inline(always)]
98pub fn lean_usize_dec_le(a1: usize, a2: usize) -> usize {
99    (a1 <= a2) as usize
100}
101
102#[inline]
103pub fn lean_usize_to_uint8(a: usize) -> u8 {
104    a as u8
105}
106#[inline]
107pub fn lean_usize_to_uint16(a: usize) -> u16 {
108    a as u16
109}
110#[inline]
111pub fn lean_usize_to_uint32(a: usize) -> u32 {
112    a as u32
113}
114#[inline]
115pub fn lean_usize_to_uint64(a: usize) -> u64 {
116    a as u64
117}
118
119extern "C" {
120    pub fn lean_usize_of_big_nat(a: b_lean_obj_arg) -> usize;
121    pub fn lean_usize_mix_hash(a1: usize, a2: usize) -> usize;
122}
lean_sys/primitive/usize_.rs

lean_sys/primitive/
usize_.rs
