blob: cc0bbcf6280390baa4c1955f94edee965f069f88 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Require Import Floats.
Open Scope float_scope.
Definition two := Eval compute in one + one.
Definition half := Eval compute in one / two.
Check (eq_refl : 1.5 = one + half).
Check (eq_refl : 15e-1 = one + half).
Check (eq_refl : 150e-2 = one + half).
Check (eq_refl : 0.15e+1 = one + half).
Check (eq_refl : 0.15e1 = one + half).
Check (eq_refl : 0.0015e3 = one + half).
|
