From 5e83a412e68916f02d86f6e7b719cd93d50c152d Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sun, 12 Dec 2021 13:13:09 +0100 Subject: _ne conversions --- lib/Floats.v | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/lib/Floats.v b/lib/Floats.v index 9ee5302d..bc066b20 100644 --- a/lib/Floats.v +++ b/lib/Floats.v @@ -360,6 +360,15 @@ Definition to_long (f:float): option int64 := (**r conversion to signed 64-bit i Definition to_longu (f:float): option int64 := (**r conversion to unsigned 64-bit int *) option_map Int64.repr (ZofB_range _ _ f 0 Int64.max_unsigned). +Definition to_int_ne (f:float): option int := (**r conversion to signed 32-bit int *) + option_map Int.repr (ZofB_ne_range _ _ f Int.min_signed Int.max_signed). +Definition to_intu_ne (f:float): option int := (**r conversion to unsigned 32-bit int *) + option_map Int.repr (ZofB_ne_range _ _ f 0 Int.max_unsigned). +Definition to_long_ne (f:float): option int64 := (**r conversion to signed 64-bit int *) + option_map Int64.repr (ZofB_ne_range _ _ f Int64.min_signed Int64.max_signed). +Definition to_longu_ne (f:float): option int64 := (**r conversion to unsigned 64-bit int *) + option_map Int64.repr (ZofB_ne_range _ _ f 0 Int64.max_unsigned). + Definition of_int (n:int): float := (**r conversion from signed 32-bit int *) BofZ 53 1024 __ __ (Int.signed n). Definition of_intu (n:int): float:= (**r conversion from unsigned 32-bit int *) -- cgit