diff options
Diffstat (limited to 'backend/SelectLong.vp')
| -rw-r--r-- | backend/SelectLong.vp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/backend/SelectLong.vp b/backend/SelectLong.vp index 0c1cbb3..ab4ab8c 100644 --- a/backend/SelectLong.vp +++ b/backend/SelectLong.vp @@ -138,6 +138,10 @@ Definition floatoflong (arg: expr) := Eexternal hf.(i64_stod) sig_l_f (arg ::: Enil). Definition floatoflongu (arg: expr) := Eexternal hf.(i64_utod) sig_l_f (arg ::: Enil). +Definition longofsingle (arg: expr) := + longoffloat (floatofsingle arg). +Definition longuofsingle (arg: expr) := + longuoffloat (floatofsingle arg). Definition singleoflong (arg: expr) := Eexternal hf.(i64_stof) sig_l_s (arg ::: Enil). Definition singleoflongu (arg: expr) := |