lean_sys/primitive/
uint32.rs1use crate::*;
2
3#[inline]
4pub unsafe fn lean_uint32_of_nat(a: b_lean_obj_arg) -> u32 {
5 if lean_is_scalar(a) {
6 lean_unbox(a) as u32
7 } else {
8 lean_uint32_of_big_nat(a)
9 }
10}
11
12#[inline]
13pub unsafe fn lean_uint32_of_nat_mk(a: lean_obj_arg) -> u32 {
14 let r = lean_uint32_of_nat(a);
15 lean_dec(a);
16 r
17}
18
19#[inline(always)]
20pub unsafe fn lean_uint32_to_nat(a: u32) -> lean_obj_res {
21 lean_usize_to_nat(a as usize)
22}
23
24#[inline(always)]
25pub fn lean_uint32_add(a1: u32, a2: u32) -> u32 {
26 a1.wrapping_add(a2)
27}
28
29#[inline(always)]
30pub fn lean_uint32_sub(a1: u32, a2: u32) -> u32 {
31 a1.wrapping_sub(a2)
32}
33
34#[inline(always)]
35pub fn lean_uint32_mul(a1: u32, a2: u32) -> u32 {
36 a1.wrapping_mul(a2)
37}
38
39#[inline(always)]
40pub fn lean_uint32_div(a1: u32, a2: u32) -> u32 {
41 if a2 == 0 {
42 0
43 } else {
44 a1 / a2
45 }
46}
47
48#[inline(always)]
49pub fn lean_uint32_mod(a1: u32, a2: u32) -> u32 {
50 if a2 == 0 {
51 a1
52 } else {
53 a1 % a2
54 }
55}
56
57#[inline(always)]
58pub fn lean_uint32_land(a1: u32, a2: u32) -> u32 {
59 a1 & a2
60}
61
62#[inline(always)]
63pub fn lean_uint32_lor(a1: u32, a2: u32) -> u32 {
64 a1 | a2
65}
66
67#[inline(always)]
68pub fn lean_uint32_xor(a1: u32, a2: u32) -> u32 {
69 a1 ^ a2
70}
71
72#[inline(always)]
73pub fn lean_uint32_shift_left(a1: u32, a2: u32) -> u32 {
74 a1.wrapping_shl(a2)
75}
76
77#[inline(always)]
78pub fn lean_uint32_shift_right(a1: u32, a2: u32) -> u32 {
79 a1.wrapping_shr(a2)
80}
81
82#[inline(always)]
83pub fn lean_uint32_complement(a: u32) -> u32 {
84 !a
85}
86
87#[inline(always)]
88pub fn lean_uint32_neg(a: u32) -> u32 {
89 0 - a
90}
91
92#[inline(always)]
93pub fn lean_uint32_dec_eq(a1: u32, a2: u32) -> u32 {
94 (a1 == a2) as u32
95}
96
97#[inline(always)]
98pub fn lean_uint32_dec_lt(a1: u32, a2: u32) -> u32 {
99 (a1 < a2) as u32
100}
101
102#[inline(always)]
103pub fn lean_uint32_dec_le(a1: u32, a2: u32) -> u32 {
104 (a1 <= a2) as u32
105}
106
107#[inline]
108pub fn lean_uint32_to_uint8(a: u32) -> u8 {
109 a as u8
110}
111#[inline]
112pub fn lean_uint32_to_uint16(a: u32) -> u16 {
113 a as u16
114}
115#[inline]
116pub fn lean_uint32_to_uint64(a: u32) -> u64 {
117 a as u64
118}
119#[inline]
120pub fn lean_uint32_to_usize(a: u32) -> usize {
121 a as usize
122}
123
124extern "C" {
125 pub fn lean_uint32_of_big_nat(a: b_lean_obj_arg) -> u32;
126}