aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Int63Syntax.out
diff options
context:
space:
mode:
authorErik Martin-Dorel2019-04-02 13:59:06 +0200
committerErik Martin-Dorel2019-04-06 13:39:52 +0200
commitf0da709639044eab19ff7d6155ccf99740f9f89a (patch)
tree2be3ef79cc9961f72a3f8ceeb76b35106b81af03 /test-suite/output/Int63Syntax.out
parent3c06ce8dc3a95e5dfe3a4c0a9acdc7dd5dac75cb (diff)
Fix pretty-printing of primitive integers
A scope delimiter was missing for primitive integers constants. Add related regression tests.
Diffstat (limited to 'test-suite/output/Int63Syntax.out')
-rw-r--r--test-suite/output/Int63Syntax.out16
1 files changed, 16 insertions, 0 deletions
diff --git a/test-suite/output/Int63Syntax.out b/test-suite/output/Int63Syntax.out
index fdd5599565..4d76f1210b 100644
--- a/test-suite/output/Int63Syntax.out
+++ b/test-suite/output/Int63Syntax.out
@@ -1,3 +1,7 @@
+2%int63
+ : int
+(2 + 2)%int63
+ : int
2
: int
9223372036854775807
@@ -14,3 +18,15 @@ The command has indeed failed with message:
int63 are only non-negative numbers.
The command has indeed failed with message:
overflow in int63 literal: 9223372036854775808
+2
+ : nat
+2%int63
+ : int
+t = 2%i63
+ : int
+t = 2%i63
+ : int
+2
+ : nat
+2
+ : int