diff options
| author | Vincent Laporte | 2020-12-02 16:57:04 +0100 |
|---|---|---|
| committer | Vincent Laporte | 2020-12-02 16:57:04 +0100 |
| commit | 11730fa0ed2cb10da1ffc00f4f1140572134937e (patch) | |
| tree | 775a310bd094e5c9149ef353abc251e8e5d657cc /test-suite/output/Int63Syntax.v | |
| parent | ad8cf0108e628710128e5a6e266b72895eed98b9 (diff) | |
| parent | 853b838681db635f51fc3c7ba3dfe26bc6712d72 (diff) | |
Merge PR #13275: Put all Int63 primitives in a separate file
Ack-by: SkySkimmer
Ack-by: ppedrot
Reviewed-by: vbgl
Diffstat (limited to 'test-suite/output/Int63Syntax.v')
| -rw-r--r-- | test-suite/output/Int63Syntax.v | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/test-suite/output/Int63Syntax.v b/test-suite/output/Int63Syntax.v index c49616d918..6f1046f7a5 100644 --- a/test-suite/output/Int63Syntax.v +++ b/test-suite/output/Int63Syntax.v @@ -1,7 +1,6 @@ -Require Import Int63 Cyclic63. +Require Import PrimInt63. Check 2%int63. -Check (2 + 2)%int63. Open Scope int63_scope. Check 2. Check 9223372036854775807. @@ -18,10 +17,7 @@ Fail Check 0xg. Fail Check 0xG. Fail Check 00x1. Fail Check 0x. -Check (Int63.add 2 2). -Check (2+2). -Eval vm_compute in 2+2. -Eval vm_compute in 65675757 * 565675998. +Check (PrimInt63.add 2 2). Fail Check -1. Fail Check 9223372036854775808. Open Scope nat_scope. @@ -36,3 +32,11 @@ Check 2. Close Scope nat_scope. Check 2. Close Scope int63_scope. + +Require Import Int63. + +Check (2 + 2)%int63. +Open Scope int63_scope. +Check (2+2). +Eval vm_compute in 2+2. +Eval vm_compute in 65675757 * 565675998. |