lean_sys/primitive/
uint64.rs

1use crate::*;
2
3#[inline]
4pub unsafe fn lean_uint64_of_nat(a: b_lean_obj_arg) -> u64 {
5    if lean_is_scalar(a) {
6        lean_unbox(a) as u64
7    } else {
8        lean_uint64_of_big_nat(a)
9    }
10}
11
12#[inline]
13pub unsafe fn lean_uint64_of_nat_mk(a: lean_obj_arg) -> u64 {
14    let r = lean_uint64_of_nat(a);
15    lean_dec(a);
16    r
17}
18
19#[inline(always)]
20pub fn lean_uint64_add(a1: u64, a2: u64) -> u64 {
21    a1.wrapping_add(a2)
22}
23
24#[inline(always)]
25pub fn lean_uint64_sub(a1: u64, a2: u64) -> u64 {
26    a1.wrapping_sub(a2)
27}
28
29#[inline(always)]
30pub fn lean_uint64_mul(a1: u64, a2: u64) -> u64 {
31    a1.wrapping_mul(a2)
32}
33
34#[inline(always)]
35pub fn lean_uint64_div(a1: u64, a2: u64) -> u64 {
36    if a2 == 0 {
37        0
38    } else {
39        a1 / a2
40    }
41}
42
43#[inline(always)]
44pub fn lean_uint64_mod(a1: u64, a2: u64) -> u64 {
45    if a2 == 0 {
46        a1
47    } else {
48        a1 % a2
49    }
50}
51
52#[inline(always)]
53pub fn lean_uint64_land(a1: u64, a2: u64) -> u64 {
54    a1 & a2
55}
56
57#[inline(always)]
58pub fn lean_uint64_lor(a1: u64, a2: u64) -> u64 {
59    a1 | a2
60}
61
62#[inline(always)]
63pub fn lean_uint64_xor(a1: u64, a2: u64) -> u64 {
64    a1 ^ a2
65}
66
67#[inline(always)]
68pub fn lean_uint64_shift_left(a1: u64, a2: u64) -> u64 {
69    a1.wrapping_shl(a2 as u32)
70}
71
72#[inline(always)]
73pub fn lean_uint64_shift_right(a1: u64, a2: u64) -> u64 {
74    a1.wrapping_shr(a2 as u32)
75}
76
77#[inline(always)]
78pub fn lean_uint64_complement(a: u64) -> u64 {
79    !a
80}
81
82#[inline(always)]
83pub fn lean_uint64_neg(a: u64) -> u64 {
84    0 - a
85}
86
87#[inline(always)]
88pub fn lean_uint64_dec_eq(a1: u64, a2: u64) -> u64 {
89    (a1 == a2) as u64
90}
91
92#[inline(always)]
93pub fn lean_uint64_dec_lt(a1: u64, a2: u64) -> u64 {
94    (a1 < a2) as u64
95}
96
97#[inline(always)]
98pub fn lean_uint64_dec_le(a1: u64, a2: u64) -> u64 {
99    (a1 <= a2) as u64
100}
101
102#[inline]
103pub fn lean_uint64_to_uint8(a: u64) -> u8 {
104    a as u8
105}
106
107#[inline]
108pub fn lean_uint64_to_uint16(a: u64) -> u16 {
109    a as u16
110}
111
112#[inline]
113pub fn lean_uint64_to_uint32(a: u64) -> u32 {
114    a as u32
115}
116
117#[inline]
118pub fn lean_uint64_to_usize(a: u64) -> usize {
119    a as usize
120}
121
122extern "C" {
123    pub fn lean_uint64_of_big_nat(a: b_lean_obj_arg) -> u64;
124    pub fn lean_uint64_mix_hash(a1: u64, a2: u64) -> u64;
125}
lean_sys/primitive/uint64.rs

lean_sys/primitive/
uint64.rs
