blob: 01a5161ef4729b166efa50a6b56717495f22c105 (
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
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
|
(* Taken from bedrock2 *)
(* Note: not an utf8 file *)
Require Import Coq.ZArith.BinInt Coq.Lists.List.
Require Coq.Init.Byte Coq.Strings.Byte Coq.Strings.String.
Definition allBytes: list Byte.byte :=
map (fun nn => match Byte.of_N (BinNat.N.of_nat nn) with
| Some b => b
| None => Byte.x00 (* won't happen *)
end)
(seq 32 95).
Notation "a b" := (@cons Byte.byte a b)
(only printing, right associativity, at level 3, format "a b").
Notation "" := (@nil Byte.byte)
(only printing, right associativity, at level 3, format "").
Notation " " := (Byte.x20) (only printing).
Notation "'!'" := (Byte.x21) (only printing).
Notation "'""'" := (Byte.x22) (only printing).
Notation "'#'" := (Byte.x23) (only printing).
Notation "'$'" := (Byte.x24) (only printing).
Notation "'%'" := (Byte.x25) (only printing).
Notation "'&'" := (Byte.x26) (only printing).
Notation "'''" := (Byte.x27) (only printing).
Notation "'('" := (Byte.x28) (only printing).
Notation "')'" := (Byte.x29) (only printing).
Notation "'*'" := (Byte.x2a) (only printing).
Notation "'+'" := (Byte.x2b) (only printing).
Notation "','" := (Byte.x2c) (only printing).
Notation "'-'" := (Byte.x2d) (only printing).
Notation "'.'" := (Byte.x2e) (only printing).
Notation "'/'" := (Byte.x2f) (only printing).
Notation "'0'" := (Byte.x30) (only printing).
Notation "'1'" := (Byte.x31) (only printing).
Notation "'2'" := (Byte.x32) (only printing).
Notation "'3'" := (Byte.x33) (only printing).
Notation "'4'" := (Byte.x34) (only printing).
Notation "'5'" := (Byte.x35) (only printing).
Notation "'6'" := (Byte.x36) (only printing).
Notation "'7'" := (Byte.x37) (only printing).
Notation "'8'" := (Byte.x38) (only printing).
Notation "'9'" := (Byte.x39) (only printing).
Notation "':'" := (Byte.x3a) (only printing).
Notation "';'" := (Byte.x3b) (only printing).
Notation "'<'" := (Byte.x3c) (only printing).
Notation "'='" := (Byte.x3d) (only printing).
Notation "'>'" := (Byte.x3e) (only printing).
Notation "'?'" := (Byte.x3f) (only printing).
Notation "'@'" := (Byte.x40) (only printing).
Notation "'A'" := (Byte.x41) (only printing).
Notation "'B'" := (Byte.x42) (only printing).
Notation "'C'" := (Byte.x43) (only printing).
Notation "'D'" := (Byte.x44) (only printing).
Notation "'E'" := (Byte.x45) (only printing).
Notation "'F'" := (Byte.x46) (only printing).
Notation "'G'" := (Byte.x47) (only printing).
Notation "'H'" := (Byte.x48) (only printing).
Notation "'I'" := (Byte.x49) (only printing).
Notation "'J'" := (Byte.x4a) (only printing).
Notation "'K'" := (Byte.x4b) (only printing).
Notation "'L'" := (Byte.x4c) (only printing).
Notation "'M'" := (Byte.x4d) (only printing).
Notation "'N'" := (Byte.x4e) (only printing).
Notation "'O'" := (Byte.x4f) (only printing).
Notation "'P'" := (Byte.x50) (only printing).
Notation "'Q'" := (Byte.x51) (only printing).
Notation "'R'" := (Byte.x52) (only printing).
Notation "'S'" := (Byte.x53) (only printing).
Notation "'T'" := (Byte.x54) (only printing).
Notation "'U'" := (Byte.x55) (only printing).
Notation "'V'" := (Byte.x56) (only printing).
Notation "'W'" := (Byte.x57) (only printing).
Notation "'X'" := (Byte.x58) (only printing).
Notation "'Y'" := (Byte.x59) (only printing).
Notation "'Z'" := (Byte.x5a) (only printing).
Notation "'['" := (Byte.x5b) (only printing).
Notation "'\'" := (Byte.x5c) (only printing).
Notation "']'" := (Byte.x5d) (only printing).
Notation "'^'" := (Byte.x5e) (only printing).
Notation "'_'" := (Byte.x5f) (only printing).
Notation "'`'" := (Byte.x60) (only printing).
Notation "'a'" := (Byte.x61) (only printing).
Notation "'b'" := (Byte.x62) (only printing).
Notation "'c'" := (Byte.x63) (only printing).
Notation "'d'" := (Byte.x64) (only printing).
Notation "'e'" := (Byte.x65) (only printing).
Notation "'f'" := (Byte.x66) (only printing).
Notation "'g'" := (Byte.x67) (only printing).
Notation "'h'" := (Byte.x68) (only printing).
Notation "'i'" := (Byte.x69) (only printing).
Notation "'j'" := (Byte.x6a) (only printing).
Notation "'k'" := (Byte.x6b) (only printing).
Notation "'l'" := (Byte.x6c) (only printing).
Notation "'m'" := (Byte.x6d) (only printing).
Notation "'n'" := (Byte.x6e) (only printing).
Notation "'o'" := (Byte.x6f) (only printing).
Notation "'p'" := (Byte.x70) (only printing).
Notation "'q'" := (Byte.x71) (only printing).
Notation "'r'" := (Byte.x72) (only printing).
Notation "'s'" := (Byte.x73) (only printing).
Notation "'t'" := (Byte.x74) (only printing).
Notation "'u'" := (Byte.x75) (only printing).
Notation "'v'" := (Byte.x76) (only printing).
Notation "'w'" := (Byte.x77) (only printing).
Notation "'x'" := (Byte.x78) (only printing).
Notation "'y'" := (Byte.x79) (only printing).
Notation "'z'" := (Byte.x7a) (only printing).
Notation "'{'" := (Byte.x7b) (only printing).
Notation "'|'" := (Byte.x7c) (only printing).
Notation "'}'" := (Byte.x7d) (only printing).
Notation "'~'" := (Byte.x7e) (only printing).
Global Set Printing Width 300.
Goal False.
let cc := eval cbv in allBytes in idtac cc.
Abort.
|
