diff options
| author | Hugo Herbelin | 2020-05-15 16:51:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-15 16:51:29 +0200 |
| commit | a5c9ad83071c99110fed464a0b9a0f5e73f1be9b (patch) | |
| tree | 4e436ada97fc8e74311e8c77312e164772957ac9 /test-suite/output/RealSyntax.out | |
| parent | b5b6e2d4c8347cb25da6f827a6b6f06cb0f566e5 (diff) | |
| parent | 31f5e89eaefcff04a04850d77b0c83cb24602f98 (diff) | |
Merge PR #11948: Hexadecimal numerals
Reviewed-by: JasonGross
Ack-by: Zimmi48
Ack-by: herbelin
Diffstat (limited to 'test-suite/output/RealSyntax.out')
| -rw-r--r-- | test-suite/output/RealSyntax.out | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test-suite/output/RealSyntax.out b/test-suite/output/RealSyntax.out index 1685964b0f..a9386b2781 100644 --- a/test-suite/output/RealSyntax.out +++ b/test-suite/output/RealSyntax.out @@ -20,3 +20,18 @@ eq_refl : -1e-4 = -1e-4 : -1e-4 = -1e-4 eq_refl : -0.50 = -0.50 : -0.50 = -0.50 +eq_refl : -26 = -26 + : -26 = -26 +eq_refl : 2860 / IZR (BinIntDef.Z.pow_pos 2 8) = 2860 / IZR (Z.pow_pos 2 8) + : 2860 / IZR (BinIntDef.Z.pow_pos 2 8) = 2860 / IZR (Z.pow_pos 2 8) +eq_refl : -6882 = -6882 + : -6882 = -6882 +eq_refl : 2860 / IZR (BinIntDef.Z.pow_pos 2 6) = 2860 / IZR (Z.pow_pos 2 6) + : 2860 / IZR (BinIntDef.Z.pow_pos 2 6) = 2860 / IZR (Z.pow_pos 2 6) +eq_refl : 2860 = 2860 + : 2860 = 2860 +eq_refl +: +-2860 / IZR (BinIntDef.Z.pow_pos 2 10) = - (2860) / IZR (Z.pow_pos 2 10) + : -2860 / IZR (BinIntDef.Z.pow_pos 2 10) = + - (2860) / IZR (Z.pow_pos 2 10) |