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
|
Require Import PArith.
Check 32%positive.
Check (eq_refl : 0x2a%positive = 42%positive).
Check (fun f : nat -> positive => (f 0%nat + 1)%positive).
Check (fun x : positive => xO x).
Check (fun x : positive => (x + 1)%positive).
Check (fun x : positive => x).
Check (fun x : positive => xI x).
Check (fun x : positive => (xO x + 1)%positive).
Check (Pos.of_nat 0 + 1)%positive.
Check (1 + Pos.of_nat (0 + 0))%positive.
Check (Pos.of_nat 1 = 1%positive).
Fail Check 0%positive.
Fail Check 0x0%positive.
Fail Check 0x00%positive.
Check 0x01%positive.
Check 0x02%positive.
Check 0xff%positive.
Check 0xFF%positive.
Check 0x01%xpositive.
Check 0x02%xpositive.
Check 0xff%xpositive.
Check 0xFF%xpositive.
(* Check hexadecimal printing *)
Open Scope hex_positive_scope.
Check 42%positive.
Check 1%positive.
Fail Check 0x0%positive.
Fail Check 0x00%positive.
Check 0x01%positive.
Check 0x02%positive.
Check 0xff%positive.
Check 0xFF%positive.
Fail Check 0x0.
Fail Check 0x00.
Check 0x01.
Check 0x02.
Check 0xff.
Check 0xFF.
Fail Check 0x0%xpositive.
Fail Check 0x00%xpositive.
Check 0x01%xpositive.
Check 0x02%xpositive.
Check 0xff%xpositive.
Check 0xFF%xpositive.
Close Scope hex_positive_scope.
Require Import Arith.
Check (1 + Pos.of_nat 11)%positive.
|
