blob: b5c6222bbacd297c115d7658b6e9de0a5256654f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Require Import QArith.
Open Scope Q_scope.
Check (eq_refl : 1.02 = 102 # 100).
Check (eq_refl : 1.02e1 = 102 # 10).
Check (eq_refl : 1.02e+03 = 1020).
Check (eq_refl : 1.02e+02 = 102 # 1).
Check (eq_refl : 10.2e-1 = 1.02).
Check (eq_refl : -0.0001 = -1 # 10000).
Check (eq_refl : -0.50 = - 50 # 100).
Check (eq_refl : -0x1a = - 26 # 1).
Check (eq_refl : 0xb.2c = 2860 # 256).
Check (eq_refl : -0x1ae2 = -6882).
Check (eq_refl : 0xb.2cp2 = 2860 # 64).
Check (eq_refl : 0xb.2cp8 = 2860).
Check (eq_refl : -0xb.2cp-2 = -2860 # 1024).
|
