diff options
Diffstat (limited to 'test-suite/output/NumbersSyntax.v')
| -rw-r--r-- | test-suite/output/NumbersSyntax.v | 30 |
1 files changed, 17 insertions, 13 deletions
diff --git a/test-suite/output/NumbersSyntax.v b/test-suite/output/NumbersSyntax.v index 3f6a40bcb7..4fbf56ab1d 100644 --- a/test-suite/output/NumbersSyntax.v +++ b/test-suite/output/NumbersSyntax.v @@ -9,8 +9,8 @@ Check 2. Check 1000000000000000000. (* = 660865024, after modulo 2^31 *) Check (add31 2 2). Check (2+2). -Eval compute in 2+2. -Eval compute in 65675757 * 565675998. +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. Close Scope int31_scope. Open Scope bigN_scope. @@ -18,8 +18,9 @@ Check 2. Check 1000000000000000000. Check (BigN.add 2 2). Check (2+2). -Eval compute in 2+2. -Eval compute in 65675757 * 565675998. +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. +Eval vm_compute in 2^100. Close Scope bigN_scope. Open Scope bigZ_scope. @@ -27,20 +28,23 @@ Check 2. Check -1000000000000000000. Check (BigZ.add 2 2). Check (2+2). -Eval compute in 2+2. -Eval compute in 65675757 * 565675998. -Close Scope bigN_scope. +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. +Eval vm_compute in (-2)^100. +Close Scope bigZ_scope. Open Scope bigQ_scope. Check 2. Check -1000000000000000000. Check (BigQ.add 2 2). Check (2+2). -Eval compute in 2+2. -Eval compute in 65675757 * 565675998. +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. (* fractions *) -Check (BigQ.Qq 6562%bigZ 456%bigN). - (* Having to say %bigZ and %bigN is a BUG! *) -Eval compute in (BigQ.red (BigQ.Qq 6562%bigZ 456%bigN)). -Eval compute in (1/10000). +Check (6562 # 456). (* Nota: # is BigQ.Qq i.e. base fractions *) +Eval vm_compute in (BigQ.red (6562 # 456)). +Eval vm_compute in (1/-10000). +Eval vm_compute in (BigQ.red (1/(1/100))). (* back to integers... *) +Eval vm_compute in ((2/3)^(-100)). +Eval vm_compute in BigQ.red ((2/3)^(-1000) * (2/3)^(1000)). Close Scope bigQ_scope. |