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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
|
Require Import Sint63.
Check 2%sint63.
Open Scope sint63_scope.
Check 2.
Check -3.
Check 4611686018427387903.
Check -4611686018427387904.
Check 0x1ab.
Check 0X1ab.
Check 0x1Ab.
Check 0x1aB.
Check 0x1AB.
Fail Check 0x1ap5. (* exponents not implemented (yet?) *)
Fail Check 0x1aP5.
Check 0x0.
Check 0x000.
Fail Check 0xg.
Fail Check 0xG.
Fail Check 00x1.
Fail Check 0x.
Check (PrimInt63.add 2 2).
Fail Check 4611686018427387904.
Fail Check -4611686018427387905.
Set Printing All.
Check 1%sint63.
Check (-1)%sint63.
Unset Printing All.
Open Scope nat_scope.
Check 2. (* : nat *)
Check 2%sint63.
Delimit Scope sint63_scope with si63.
Definition t := 2%sint63.
Print t.
Delimit Scope nat_scope with sint63.
Print t.
Check 2.
Close Scope nat_scope.
Check 2.
Close Scope sint63_scope.
Delimit Scope sint63_scope with sint63.
Check (2 + 2)%sint63.
Open Scope sint63_scope.
Check (2+2).
Eval vm_compute in 2+2.
Eval vm_compute in 65675757 * 565675998.
|
