lean_sys/primitive/
float32.rs

1use crate::*;
2
3pub fn lean_float32_to_uint8(a: f32) -> u8 {
4    //NOTE: this performs a saturating cast, as desired
5    a as u8
6}
7pub fn lean_float32_to_uint16(a: f32) -> u16 {
8    //NOTE: this performs a saturating cast, as desired
9    a as u16
10}
11pub fn lean_float32_to_uint32(a: f32) -> u32 {
12    //NOTE: this performs a saturating cast, as desired
13    a as u32
14}
15pub fn lean_float32_to_uint64(a: f32) -> u64 {
16    //NOTE: this performs a saturating cast, as desired
17    a as u64
18}
19pub fn lean_float32_to_usize(a: f32) -> usize {
20    //NOTE: this performs a saturating cast, as desired
21    a as usize
22}
23pub fn lean_float32_add(a: f32, b: f32) -> f32 {
24    a + b
25}
26pub fn lean_float32_sub(a: f32, b: f32) -> f32 {
27    a - b
28}
29pub fn lean_float32_mul(a: f32, b: f32) -> f32 {
30    a * b
31}
32pub fn lean_float32_div(a: f32, b: f32) -> f32 {
33    a / b
34}
35pub fn lean_float32_negate(a: f32) -> f32 {
36    -a
37}
38pub fn lean_float32_beq(a: f32, b: f32) -> u8 {
39    (a == b) as u8
40}
41pub fn lean_float32_decLe(a: f32, b: f32) -> u8 {
42    (a <= b) as u8
43}
44pub fn lean_float32_decLt(a: f32, b: f32) -> u8 {
45    (a < b) as u8
46}
47pub fn lean_uint64_to_float32(a: u64) -> f32 {
48    a as f32
49}
50
51pub fn lean_float_to_float32(a: f64) -> f32 {
52    a as f32
53}
54pub fn lean_float32_to_float(a: f32) -> f64 {
55    a as f64
56}
57
58extern "C" {
59    pub fn lean_float32_to_string(a: f32) -> lean_obj_res;
60    pub fn lean_float32_scaleb(a: f32, b: b_lean_obj_arg) -> f32;
61    pub fn lean_float32_isnan(a: f32) -> u8;
62    pub fn lean_float32_isfinite(a: f32) -> u8;
63    pub fn lean_float32_isinf(a: f32) -> u8;
64    pub fn lean_float32_frexp(a: f32) -> lean_obj_res;
65    pub fn lean_float32_of_bits(a: u32) -> f32;
66    pub fn lean_float32_to_bits(a: f32) -> u32;
67}
lean_sys/primitive/float32.rs

lean_sys/primitive/
float32.rs
