blob: be0ee701afbffd3dcf311f5893aab41c23bbc92d (
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
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
Require Import PrimInt63.
Check 2%int63.
Open Scope int63_scope.
Check 2.
Check 9223372036854775807.
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 -1.
Fail Check 9223372036854775808.
Set Printing All.
Check 1%int63.
Unset Printing All.
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.
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.
Eval simpl in 2+2.
Eval hnf in 2+2.
Eval cbn in 2+2.
Eval hnf in PrimInt63.add.
Eval simpl in (2 * 3) + (2 * 3).
Eval hnf in (2 * 3) + (2 * 3).
Eval cbn in (2 * 3) + (2 * 3).
Section TestNoSimpl.
Variable x : int.
Eval simpl in 1 + 2 + x.
Eval hnf in 1 + 2 + x.
End TestNoSimpl.
|
