diff options
Diffstat (limited to 'common')
-rw-r--r-- | common/Values.v | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/common/Values.v b/common/Values.v index 7caf5515..b937071c 100644 --- a/common/Values.v +++ b/common/Values.v @@ -438,6 +438,18 @@ Definition floatoflongu (v: val) : option val := | _ => None end. +Definition singleoflong (v: val) : option val := + match v with + | Vlong n => Some (Vfloat (Float.singleoflong n)) + | _ => None + end. + +Definition singleoflongu (v: val) : option val := + match v with + | Vlong n => Some (Vfloat (Float.singleoflongu n)) + | _ => None + end. + Definition addl (v1 v2: val): val := match v1, v2 with | Vlong n1, Vlong n2 => Vlong(Int64.add n1 n2) |