aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Int63Syntax.v
blob: 3dc364eddb09b4c53c9125b7c541a5dd8efb5712 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
Require Import Int63 Cyclic63.

Open Scope int63_scope.
Check 2.
Check 9223372036854775807.
Check (Int63.add 2 2).
Check (2+2).
Eval vm_compute in 2+2.
Eval vm_compute in 65675757 * 565675998.
Fail Check -1.
Fail Check 9223372036854775808.
Close Scope int63_scope.