blob: 0385e529bf7f572d571767b138aca4533230658d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
Require Import Int63 Cyclic63.
Check 2%int63.
Check (2 + 2)%int63.
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.
Open Scope nat_scope.
Check 2. (* : nat *)
Check 2%int63.
Delimit Scope int63_scope with i63.
Definition t := 2%int63.
Print t.
Delimit Scope nat_scope with int63.
Print t.
Check 2.
Close Scope nat_scope.
Check 2.
Close Scope int63_scope.
|
