Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`

3 files changed, 1154 insertions, 3 deletions

diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 7446c17d98..f4544a0df3 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -34,17 +34,23 @@ bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
 bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
 eq_true_rec:
   forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
-eq_true_ind:
-  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
+bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
 eq_true_rect_r:
   forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
 eq_true_rec_r:
   forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
 eq_true_rect:
   forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
-bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
+eq_true_ind:
+  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
 eq_true_ind_r:
   forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
+Byte.to_bits:
+  Byte.byte ->
+  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
+Byte.of_bits:
+  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))) ->
+  Byte.byte
 andb_true_intro:
   forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
 andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
@@ -52,6 +58,10 @@ BoolSpec_ind:
   forall (P Q : Prop) (P0 : bool -> Prop),
   (P -> P0 true) ->
   (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
+Byte.to_bits_of_bits:
+  forall
+    b : bool * (bool * (bool * (bool * (bool * (bool * (bool * bool)))))),
+  Byte.to_bits (Byte.of_bits b) = b
 bool_choice:
   forall (S : Set) (R1 R2 : S -> Prop),
   (forall x : S, {R1 x} + {R2 x}) ->
diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out
new file mode 100644
index 0000000000..bbc936766d
--- /dev/null
+++ b/test-suite/output/StringSyntax.out
@@ -0,0 +1,1089 @@
+Monomorphic byte_rect = 
+fun (P : byte -> Type) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") 
+  (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") 
+  (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") 
+  (f187 : P "188") (f188 : P "189") (f189 : P "190") (f190 : P "191") (f191 : P "192") (f192 : P "193") (f193 : P "194") (f194 : P "195") (f195 : P "196") (f196 : P "197") (f197 : P "198") (f198 : P "199") (f199 : P "200") (f200 : P "201") (f201 : P "202") (f202 : P "203") (f203 : P "204") (f204 : P "205") (f205 : P "206") (f206 : P "207") (f207 : P "208") (f208 : P "209") (f209 : P "210") (f210 : P "211") (f211 : P "212") (f212 : P "213") (f213 : P "214") (f214 : P "215") (f215 : P "216") (f216 : P "217") (f217 : P "218") (f218 : P "219") (f219 : P "220") (f220 : P "221") (f221 : P "222") (f222 : P "223") (f223 : P "224") (f224 : P "225") (f225 : P "226") (f226 : P "227") (f227 : P "228") (f228 : P "229") (f229 : P "230") (f230 : P "231") (f231 : P "232") (f232 : P "233") (f233 : P "234") (f234 : P "235") (f235 : P "236") (f236 : P "237") (f237 : P "238") (f238 : P "239") (f239 : P "240") (f240 : P "241") (f241 : P "242") (f242 : P "243") (f243 : P "244") 
+  (f244 : P "245") (f245 : P "246") (f246 : P "247") (f247 : P "248") (f248 : P "249") (f249 : P "250") (f250 : P "251") (f251 : P "252") (f252 : P "253") (f253 : P "254") (f254 : P "255") (b : byte) =>
+match b as b0 return (P b0) with
+| "000" => f
+| "001" => f0
+| "002" => f1
+| "003" => f2
+| "004" => f3
+| "005" => f4
+| "006" => f5
+| "007" => f6
+| "008" => f7
+| "009" => f8
+| "010" => f9
+| "011" => f10
+| "012" => f11
+| "013" => f12
+| "014" => f13
+| "015" => f14
+| "016" => f15
+| "017" => f16
+| "018" => f17
+| "019" => f18
+| "020" => f19
+| "021" => f20
+| "022" => f21
+| "023" => f22
+| "024" => f23
+| "025" => f24
+| "026" => f25
+| "027" => f26
+| "028" => f27
+| "029" => f28
+| "030" => f29
+| "031" => f30
+| " " => f31
+| "!" => f32
+| """" => f33
+| "#" => f34
+| "$" => f35
+| "%" => f36
+| "&" => f37
+| "'" => f38
+| "(" => f39
+| ")" => f40
+| "*" => f41
+| "+" => f42
+| "," => f43
+| "-" => f44
+| "." => f45
+| "/" => f46
+| "0" => f47
+| "1" => f48
+| "2" => f49
+| "3" => f50
+| "4" => f51
+| "5" => f52
+| "6" => f53
+| "7" => f54
+| "8" => f55
+| "9" => f56
+| ":" => f57
+| ";" => f58
+| "<" => f59
+| "=" => f60
+| ">" => f61
+| "?" => f62
+| "@" => f63
+| "A" => f64
+| "B" => f65
+| "C" => f66
+| "D" => f67
+| "E" => f68
+| "F" => f69
+| "G" => f70
+| "H" => f71
+| "I" => f72
+| "J" => f73
+| "K" => f74
+| "L" => f75
+| "M" => f76
+| "N" => f77
+| "O" => f78
+| "P" => f79
+| "Q" => f80
+| "R" => f81
+| "S" => f82
+| "T" => f83
+| "U" => f84
+| "V" => f85
+| "W" => f86
+| "X" => f87
+| "Y" => f88
+| "Z" => f89
+| "[" => f90
+| "\" => f91
+| "]" => f92
+| "^" => f93
+| "_" => f94
+| "`" => f95
+| "a" => f96
+| "b" => f97
+| "c" => f98
+| "d" => f99
+| "e" => f100
+| "f" => f101
+| "g" => f102
+| "h" => f103
+| "i" => f104
+| "j" => f105
+| "k" => f106
+| "l" => f107
+| "m" => f108
+| "n" => f109
+| "o" => f110
+| "p" => f111
+| "q" => f112
+| "r" => f113
+| "s" => f114
+| "t" => f115
+| "u" => f116
+| "v" => f117
+| "w" => f118
+| "x" => f119
+| "y" => f120
+| "z" => f121
+| "{" => f122
+| "|" => f123
+| "}" => f124
+| "~" => f125
+| "127" => f126
+| "128" => f127
+| "129" => f128
+| "130" => f129
+| "131" => f130
+| "132" => f131
+| "133" => f132
+| "134" => f133
+| "135" => f134
+| "136" => f135
+| "137" => f136
+| "138" => f137
+| "139" => f138
+| "140" => f139
+| "141" => f140
+| "142" => f141
+| "143" => f142
+| "144" => f143
+| "145" => f144
+| "146" => f145
+| "147" => f146
+| "148" => f147
+| "149" => f148
+| "150" => f149
+| "151" => f150
+| "152" => f151
+| "153" => f152
+| "154" => f153
+| "155" => f154
+| "156" => f155
+| "157" => f156
+| "158" => f157
+| "159" => f158
+| "160" => f159
+| "161" => f160
+| "162" => f161
+| "163" => f162
+| "164" => f163
+| "165" => f164
+| "166" => f165
+| "167" => f166
+| "168" => f167
+| "169" => f168
+| "170" => f169
+| "171" => f170
+| "172" => f171
+| "173" => f172
+| "174" => f173
+| "175" => f174
+| "176" => f175
+| "177" => f176
+| "178" => f177
+| "179" => f178
+| "180" => f179
+| "181" => f180
+| "182" => f181
+| "183" => f182
+| "184" => f183
+| "185" => f184
+| "186" => f185
+| "187" => f186
+| "188" => f187
+| "189" => f188
+| "190" => f189
+| "191" => f190
+| "192" => f191
+| "193" => f192
+| "194" => f193
+| "195" => f194
+| "196" => f195
+| "197" => f196
+| "198" => f197
+| "199" => f198
+| "200" => f199
+| "201" => f200
+| "202" => f201
+| "203" => f202
+| "204" => f203
+| "205" => f204
+| "206" => f205
+| "207" => f206
+| "208" => f207
+| "209" => f208
+| "210" => f209
+| "211" => f210
+| "212" => f211
+| "213" => f212
+| "214" => f213
+| "215" => f214
+| "216" => f215
+| "217" => f216
+| "218" => f217
+| "219" => f218
+| "220" => f219
+| "221" => f220
+| "222" => f221
+| "223" => f222
+| "224" => f223
+| "225" => f224
+| "226" => f225
+| "227" => f226
+| "228" => f227
+| "229" => f228
+| "230" => f229
+| "231" => f230
+| "232" => f231
+| "233" => f232
+| "234" => f233
+| "235" => f234
+| "236" => f235
+| "237" => f236
+| "238" => f237
+| "239" => f238
+| "240" => f239
+| "241" => f240
+| "242" => f241
+| "243" => f242
+| "244" => f243
+| "245" => f244
+| "246" => f245
+| "247" => f246
+| "248" => f247
+| "249" => f248
+| "250" => f249
+| "251" => f250
+| "252" => f251
+| "253" => f252
+| "254" => f253
+| "255" => f254
+end
+     : forall P : byte -> Type,
+       P "000" ->
+       P "001" ->
+       P "002" ->
+       P "003" ->
+       P "004" ->
+       P "005" ->
+       P "006" ->
+       P "007" ->
+       P "008" ->
+       P "009" ->
+       P "010" ->
+       P "011" ->
+       P "012" ->
+       P "013" ->
+       P "014" ->
+       P "015" ->
+       P "016" ->
+       P "017" ->
+       P "018" ->
+       P "019" ->
+       P "020" ->
+       P "021" ->
+       P "022" ->
+       P "023" ->
+       P "024" ->
+       P "025" ->
+       P "026" ->
+       P "027" ->
+       P "028" ->
+       P "029" ->
+       P "030" ->
+       P "031" ->
+       P " " ->
+       P "!" ->
+       P """" ->
+       P "#" ->
+       P "$" ->
+       P "%" ->
+       P "&" ->
+       P "'" ->
+       P "(" ->
+       P ")" ->
+       P "*" ->
+       P "+" ->
+       P "," ->
+       P "-" ->
+       P "." ->
+       P "/" ->
+       P "0" ->
+       P "1" ->
+       P "2" ->
+       P "3" ->
+       P "4" ->
+       P "5" ->
+       P "6" ->
+       P "7" ->
+       P "8" ->
+       P "9" ->
+       P ":" ->
+       P ";" ->
+       P "<" ->
+       P "=" ->
+       P ">" ->
+       P "?" ->
+       P "@" ->
+       P "A" ->
+       P "B" ->
+       P "C" ->
+       P "D" ->
+       P "E" ->
+       P "F" ->
+       P "G" ->
+       P "H" ->
+       P "I" ->
+       P "J" ->
+       P "K" ->
+       P "L" ->
+       P "M" ->
+       P "N" ->
+       P "O" ->
+       P "P" ->
+       P "Q" ->
+       P "R" ->
+       P "S" ->
+       P "T" ->
+       P "U" ->
+       P "V" ->
+       P "W" ->
+       P "X" ->
+       P "Y" ->
+       P "Z" ->
+       P "[" ->
+       P "\" ->
+       P "]" ->
+       P "^" ->
+       P "_" ->
+       P "`" ->
+       P "a" ->
+       P "b" ->
+       P "c" ->
+       P "d" ->
+       P "e" ->
+       P "f" ->
+       P "g" ->
+       P "h" ->
+       P "i" ->
+       P "j" ->
+       P "k" ->
+       P "l" ->
+       P "m" ->
+       P "n" ->
+       P "o" ->
+       P "p" ->
+       P "q" ->
+       P "r" ->
+       P "s" ->
+       P "t" ->
+       P "u" ->
+       P "v" ->
+       P "w" ->
+       P "x" ->
+       P "y" ->
+       P "z" ->
+       P "{" ->
+       P "|" ->
+       P "}" ->
+       P "~" ->
+       P "127" ->
+       P "128" ->
+       P "129" ->
+       P "130" ->
+       P "131" ->
+       P "132" ->
+       P "133" ->
+       P "134" ->
+       P "135" ->
+       P "136" ->
+       P "137" ->
+       P "138" ->
+       P "139" ->
+       P "140" ->
+       P "141" ->
+       P "142" ->
+       P "143" ->
+       P "144" ->
+       P "145" ->
+       P "146" ->
+       P "147" ->
+       P "148" ->
+       P "149" ->
+       P "150" ->
+       P "151" ->
+       P "152" ->
+       P "153" ->
+       P "154" ->
+       P "155" ->
+       P "156" ->
+       P "157" ->
+       P "158" ->
+       P "159" ->
+       P "160" ->
+       P "161" ->
+       P "162" ->
+       P "163" ->
+       P "164" ->
+       P "165" ->
+       P "166" ->
+       P "167" ->
+       P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
+
+byte_rect is not universe polymorphic
+Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
+Monomorphic byte_rec = 
+fun P : byte -> Set => byte_rect P
+     : forall P : byte -> Set,
+       P "000" ->
+       P "001" ->
+       P "002" ->
+       P "003" ->
+       P "004" ->
+       P "005" ->
+       P "006" ->
+       P "007" ->
+       P "008" ->
+       P "009" ->
+       P "010" ->
+       P "011" ->
+       P "012" ->
+       P "013" ->
+       P "014" ->
+       P "015" ->
+       P "016" ->
+       P "017" ->
+       P "018" ->
+       P "019" ->
+       P "020" ->
+       P "021" ->
+       P "022" ->
+       P "023" ->
+       P "024" ->
+       P "025" ->
+       P "026" ->
+       P "027" ->
+       P "028" ->
+       P "029" ->
+       P "030" ->
+       P "031" ->
+       P " " ->
+       P "!" ->
+       P """" ->
+       P "#" ->
+       P "$" ->
+       P "%" ->
+       P "&" ->
+       P "'" ->
+       P "(" ->
+       P ")" ->
+       P "*" ->
+       P "+" ->
+       P "," ->
+       P "-" ->
+       P "." ->
+       P "/" ->
+       P "0" ->
+       P "1" ->
+       P "2" ->
+       P "3" ->
+       P "4" ->
+       P "5" ->
+       P "6" ->
+       P "7" ->
+       P "8" ->
+       P "9" ->
+       P ":" ->
+       P ";" ->
+       P "<" ->
+       P "=" ->
+       P ">" ->
+       P "?" ->
+       P "@" ->
+       P "A" ->
+       P "B" ->
+       P "C" ->
+       P "D" ->
+       P "E" ->
+       P "F" ->
+       P "G" ->
+       P "H" ->
+       P "I" ->
+       P "J" ->
+       P "K" ->
+       P "L" ->
+       P "M" ->
+       P "N" ->
+       P "O" ->
+       P "P" ->
+       P "Q" ->
+       P "R" ->
+       P "S" ->
+       P "T" ->
+       P "U" ->
+       P "V" ->
+       P "W" ->
+       P "X" ->
+       P "Y" ->
+       P "Z" ->
+       P "[" ->
+       P "\" ->
+       P "]" ->
+       P "^" ->
+       P "_" ->
+       P "`" ->
+       P "a" ->
+       P "b" ->
+       P "c" ->
+       P "d" ->
+       P "e" ->
+       P "f" ->
+       P "g" ->
+       P "h" ->
+       P "i" ->
+       P "j" ->
+       P "k" ->
+       P "l" ->
+       P "m" ->
+       P "n" ->
+       P "o" ->
+       P "p" ->
+       P "q" ->
+       P "r" ->
+       P "s" ->
+       P "t" ->
+       P "u" ->
+       P "v" ->
+       P "w" ->
+       P "x" ->
+       P "y" ->
+       P "z" ->
+       P "{" ->
+       P "|" ->
+       P "}" ->
+       P "~" ->
+       P "127" ->
+       P "128" ->
+       P "129" ->
+       P "130" ->
+       P "131" ->
+       P "132" ->
+       P "133" ->
+       P "134" ->
+       P "135" ->
+       P "136" ->
+       P "137" ->
+       P "138" ->
+       P "139" ->
+       P "140" ->
+       P "141" ->
+       P "142" ->
+       P "143" ->
+       P "144" ->
+       P "145" ->
+       P "146" ->
+       P "147" ->
+       P "148" ->
+       P "149" ->
+       P "150" ->
+       P "151" ->
+       P "152" ->
+       P "153" ->
+       P "154" ->
+       P "155" ->
+       P "156" ->
+       P "157" ->
+       P "158" ->
+       P "159" ->
+       P "160" ->
+       P "161" ->
+       P "162" ->
+       P "163" ->
+       P "164" ->
+       P "165" ->
+       P "166" ->
+       P "167" ->
+       P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
+
+byte_rec is not universe polymorphic
+Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
+Monomorphic byte_ind = 
+fun (P : byte -> Prop) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") 
+  (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") 
+  (f130 : P "131") (f131 : P "132") (f132 : P "133") (f133 : P "134") (f134 : P "135") (f135 : P "136") (f136 : P "137") (f137 : P "138") (f138 : P "139") (f139 : P "140") (f140 : P "141") (f141 : P "142") (f142 : P "143") (f143 : P "144") (f144 : P "145") (f145 : P "146") (f146 : P "147") (f147 : P "148") (f148 : P "149") (f149 : P "150") (f150 : P "151") (f151 : P "152") (f152 : P "153") (f153 : P "154") (f154 : P "155") (f155 : P "156") (f156 : P "157") (f157 : P "158") (f158 : P "159") (f159 : P "160") (f160 : P "161") (f161 : P "162") (f162 : P "163") (f163 : P "164") (f164 : P "165") (f165 : P "166") (f166 : P "167") (f167 : P "168") (f168 : P "169") (f169 : P "170") (f170 : P "171") (f171 : P "172") (f172 : P "173") (f173 : P "174") (f174 : P "175") (f175 : P "176") (f176 : P "177") (f177 : P "178") (f178 : P "179") (f179 : P "180") (f180 : P "181") (f181 : P "182") (f182 : P "183") (f183 : P "184") (f184 : P "185") (f185 : P "186") (f186 : P "187") 
+  (f187 : P "188") (f188 : P "189") (f189 : P "190") (f190 : P "191") (f191 : P "192") (f192 : P "193") (f193 : P "194") (f194 : P "195") (f195 : P "196") (f196 : P "197") (f197 : P "198") (f198 : P "199") (f199 : P "200") (f200 : P "201") (f201 : P "202") (f202 : P "203") (f203 : P "204") (f204 : P "205") (f205 : P "206") (f206 : P "207") (f207 : P "208") (f208 : P "209") (f209 : P "210") (f210 : P "211") (f211 : P "212") (f212 : P "213") (f213 : P "214") (f214 : P "215") (f215 : P "216") (f216 : P "217") (f217 : P "218") (f218 : P "219") (f219 : P "220") (f220 : P "221") (f221 : P "222") (f222 : P "223") (f223 : P "224") (f224 : P "225") (f225 : P "226") (f226 : P "227") (f227 : P "228") (f228 : P "229") (f229 : P "230") (f230 : P "231") (f231 : P "232") (f232 : P "233") (f233 : P "234") (f234 : P "235") (f235 : P "236") (f236 : P "237") (f237 : P "238") (f238 : P "239") (f239 : P "240") (f240 : P "241") (f241 : P "242") (f242 : P "243") (f243 : P "244") 
+  (f244 : P "245") (f245 : P "246") (f246 : P "247") (f247 : P "248") (f248 : P "249") (f249 : P "250") (f250 : P "251") (f251 : P "252") (f252 : P "253") (f253 : P "254") (f254 : P "255") (b : byte) =>
+match b as b0 return (P b0) with
+| "000" => f
+| "001" => f0
+| "002" => f1
+| "003" => f2
+| "004" => f3
+| "005" => f4
+| "006" => f5
+| "007" => f6
+| "008" => f7
+| "009" => f8
+| "010" => f9
+| "011" => f10
+| "012" => f11
+| "013" => f12
+| "014" => f13
+| "015" => f14
+| "016" => f15
+| "017" => f16
+| "018" => f17
+| "019" => f18
+| "020" => f19
+| "021" => f20
+| "022" => f21
+| "023" => f22
+| "024" => f23
+| "025" => f24
+| "026" => f25
+| "027" => f26
+| "028" => f27
+| "029" => f28
+| "030" => f29
+| "031" => f30
+| " " => f31
+| "!" => f32
+| """" => f33
+| "#" => f34
+| "$" => f35
+| "%" => f36
+| "&" => f37
+| "'" => f38
+| "(" => f39
+| ")" => f40
+| "*" => f41
+| "+" => f42
+| "," => f43
+| "-" => f44
+| "." => f45
+| "/" => f46
+| "0" => f47
+| "1" => f48
+| "2" => f49
+| "3" => f50
+| "4" => f51
+| "5" => f52
+| "6" => f53
+| "7" => f54
+| "8" => f55
+| "9" => f56
+| ":" => f57
+| ";" => f58
+| "<" => f59
+| "=" => f60
+| ">" => f61
+| "?" => f62
+| "@" => f63
+| "A" => f64
+| "B" => f65
+| "C" => f66
+| "D" => f67
+| "E" => f68
+| "F" => f69
+| "G" => f70
+| "H" => f71
+| "I" => f72
+| "J" => f73
+| "K" => f74
+| "L" => f75
+| "M" => f76
+| "N" => f77
+| "O" => f78
+| "P" => f79
+| "Q" => f80
+| "R" => f81
+| "S" => f82
+| "T" => f83
+| "U" => f84
+| "V" => f85
+| "W" => f86
+| "X" => f87
+| "Y" => f88
+| "Z" => f89
+| "[" => f90
+| "\" => f91
+| "]" => f92
+| "^" => f93
+| "_" => f94
+| "`" => f95
+| "a" => f96
+| "b" => f97
+| "c" => f98
+| "d" => f99
+| "e" => f100
+| "f" => f101
+| "g" => f102
+| "h" => f103
+| "i" => f104
+| "j" => f105
+| "k" => f106
+| "l" => f107
+| "m" => f108
+| "n" => f109
+| "o" => f110
+| "p" => f111
+| "q" => f112
+| "r" => f113
+| "s" => f114
+| "t" => f115
+| "u" => f116
+| "v" => f117
+| "w" => f118
+| "x" => f119
+| "y" => f120
+| "z" => f121
+| "{" => f122
+| "|" => f123
+| "}" => f124
+| "~" => f125
+| "127" => f126
+| "128" => f127
+| "129" => f128
+| "130" => f129
+| "131" => f130
+| "132" => f131
+| "133" => f132
+| "134" => f133
+| "135" => f134
+| "136" => f135
+| "137" => f136
+| "138" => f137
+| "139" => f138
+| "140" => f139
+| "141" => f140
+| "142" => f141
+| "143" => f142
+| "144" => f143
+| "145" => f144
+| "146" => f145
+| "147" => f146
+| "148" => f147
+| "149" => f148
+| "150" => f149
+| "151" => f150
+| "152" => f151
+| "153" => f152
+| "154" => f153
+| "155" => f154
+| "156" => f155
+| "157" => f156
+| "158" => f157
+| "159" => f158
+| "160" => f159
+| "161" => f160
+| "162" => f161
+| "163" => f162
+| "164" => f163
+| "165" => f164
+| "166" => f165
+| "167" => f166
+| "168" => f167
+| "169" => f168
+| "170" => f169
+| "171" => f170
+| "172" => f171
+| "173" => f172
+| "174" => f173
+| "175" => f174
+| "176" => f175
+| "177" => f176
+| "178" => f177
+| "179" => f178
+| "180" => f179
+| "181" => f180
+| "182" => f181
+| "183" => f182
+| "184" => f183
+| "185" => f184
+| "186" => f185
+| "187" => f186
+| "188" => f187
+| "189" => f188
+| "190" => f189
+| "191" => f190
+| "192" => f191
+| "193" => f192
+| "194" => f193
+| "195" => f194
+| "196" => f195
+| "197" => f196
+| "198" => f197
+| "199" => f198
+| "200" => f199
+| "201" => f200
+| "202" => f201
+| "203" => f202
+| "204" => f203
+| "205" => f204
+| "206" => f205
+| "207" => f206
+| "208" => f207
+| "209" => f208
+| "210" => f209
+| "211" => f210
+| "212" => f211
+| "213" => f212
+| "214" => f213
+| "215" => f214
+| "216" => f215
+| "217" => f216
+| "218" => f217
+| "219" => f218
+| "220" => f219
+| "221" => f220
+| "222" => f221
+| "223" => f222
+| "224" => f223
+| "225" => f224
+| "226" => f225
+| "227" => f226
+| "228" => f227
+| "229" => f228
+| "230" => f229
+| "231" => f230
+| "232" => f231
+| "233" => f232
+| "234" => f233
+| "235" => f234
+| "236" => f235
+| "237" => f236
+| "238" => f237
+| "239" => f238
+| "240" => f239
+| "241" => f240
+| "242" => f241
+| "243" => f242
+| "244" => f243
+| "245" => f244
+| "246" => f245
+| "247" => f246
+| "248" => f247
+| "249" => f248
+| "250" => f249
+| "251" => f250
+| "252" => f251
+| "253" => f252
+| "254" => f253
+| "255" => f254
+end
+     : forall P : byte -> Prop,
+       P "000" ->
+       P "001" ->
+       P "002" ->
+       P "003" ->
+       P "004" ->
+       P "005" ->
+       P "006" ->
+       P "007" ->
+       P "008" ->
+       P "009" ->
+       P "010" ->
+       P "011" ->
+       P "012" ->
+       P "013" ->
+       P "014" ->
+       P "015" ->
+       P "016" ->
+       P "017" ->
+       P "018" ->
+       P "019" ->
+       P "020" ->
+       P "021" ->
+       P "022" ->
+       P "023" ->
+       P "024" ->
+       P "025" ->
+       P "026" ->
+       P "027" ->
+       P "028" ->
+       P "029" ->
+       P "030" ->
+       P "031" ->
+       P " " ->
+       P "!" ->
+       P """" ->
+       P "#" ->
+       P "$" ->
+       P "%" ->
+       P "&" ->
+       P "'" ->
+       P "(" ->
+       P ")" ->
+       P "*" ->
+       P "+" ->
+       P "," ->
+       P "-" ->
+       P "." ->
+       P "/" ->
+       P "0" ->
+       P "1" ->
+       P "2" ->
+       P "3" ->
+       P "4" ->
+       P "5" ->
+       P "6" ->
+       P "7" ->
+       P "8" ->
+       P "9" ->
+       P ":" ->
+       P ";" ->
+       P "<" ->
+       P "=" ->
+       P ">" ->
+       P "?" ->
+       P "@" ->
+       P "A" ->
+       P "B" ->
+       P "C" ->
+       P "D" ->
+       P "E" ->
+       P "F" ->
+       P "G" ->
+       P "H" ->
+       P "I" ->
+       P "J" ->
+       P "K" ->
+       P "L" ->
+       P "M" ->
+       P "N" ->
+       P "O" ->
+       P "P" ->
+       P "Q" ->
+       P "R" ->
+       P "S" ->
+       P "T" ->
+       P "U" ->
+       P "V" ->
+       P "W" ->
+       P "X" ->
+       P "Y" ->
+       P "Z" ->
+       P "[" ->
+       P "\" ->
+       P "]" ->
+       P "^" ->
+       P "_" ->
+       P "`" ->
+       P "a" ->
+       P "b" ->
+       P "c" ->
+       P "d" ->
+       P "e" ->
+       P "f" ->
+       P "g" ->
+       P "h" ->
+       P "i" ->
+       P "j" ->
+       P "k" ->
+       P "l" ->
+       P "m" ->
+       P "n" ->
+       P "o" ->
+       P "p" ->
+       P "q" ->
+       P "r" ->
+       P "s" ->
+       P "t" ->
+       P "u" ->
+       P "v" ->
+       P "w" ->
+       P "x" ->
+       P "y" ->
+       P "z" ->
+       P "{" ->
+       P "|" ->
+       P "}" ->
+       P "~" ->
+       P "127" ->
+       P "128" ->
+       P "129" ->
+       P "130" ->
+       P "131" ->
+       P "132" ->
+       P "133" ->
+       P "134" ->
+       P "135" ->
+       P "136" ->
+       P "137" ->
+       P "138" ->
+       P "139" ->
+       P "140" ->
+       P "141" ->
+       P "142" ->
+       P "143" ->
+       P "144" ->
+       P "145" ->
+       P "146" ->
+       P "147" ->
+       P "148" ->
+       P "149" ->
+       P "150" ->
+       P "151" ->
+       P "152" ->
+       P "153" ->
+       P "154" ->
+       P "155" ->
+       P "156" ->
+       P "157" ->
+       P "158" ->
+       P "159" ->
+       P "160" ->
+       P "161" ->
+       P "162" ->
+       P "163" ->
+       P "164" ->
+       P "165" ->
+       P "166" ->
+       P "167" ->
+       P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
+
+byte_ind is not universe polymorphic
+Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
+"000"
+     : byte
+"a"
+     : byte
+"127"
+     : byte
+The command has indeed failed with message:
+Expects a single character or a three-digits ascii code.
+"000"
+     : ascii
+"a"
+     : ascii
+"127"
+     : ascii
+The command has indeed failed with message:
+Expects a single character or a three-digits ascii code.
+"000"
+     : string
+"a"
+     : string
+"127"
+     : string
+"€"
+     : string
+"
"
+     : string
+     = "a"%char
+     : ascii
+     = "a"%byte
+     : byte
+     = "a"%string
+     : string
+     = ["a"%byte]
+     : list byte
+     = ["000"; "001"; "002"; "003"; "004"; "005"; "006"; "007"; "008"; "009"; "010"; "011"; "012"; "013"; "014"; "015"; "016"; "017"; "018"; "019"; "020"; "021"; "022"; "023"; "024"; "025"; "026"; "027"; "028"; "029"; "030"; "031"; " "; "!"; """"; "#"; "$"; "%"; "&"; "'"; "("; ")"; "*"; "+"; ","; "-"; "."; "/"; "0"; "1"; "2"; "3"; "4"; "5"; "6"; "7"; "8"; "9"; ":"; ";"; "<"; "="; ">"; "?"; "@"; "A"; "B"; "C"; "D"; "E"; "F"; "G"; "H"; "I"; "J"; "K"; "L"; "M"; "N"; "O"; "P"; "Q"; "R"; "S"; "T"; "U"; "V"; "W"; "X"; "Y"; "Z"; "["; "\"; "]"; "^"; "_"; "`"; "a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"; "k"; "l"; "m"; "n"; "o"; "p"; "q"; "r"; "s"; "t"; "u"; "v"; "w"; "x"; "y"; "z"; "{"; "|"; "}"; "~"; "127"; "128"; "129"; "130"; "131"; "132"; "133"; "134"; "135"; "136"; "137"; "138"; "139"; "140"; "141"; "142"; "143"; "144"; "145"; "146"; "147"; "148"; "149"; "150"; "151"; "152"; "153"; "154"; "155"; "156"; "157"; "158"; "159"; "160"; "161"; "162"; "163"; "164"; "165"; "166"; "167";
+       "168"; "169"; "170"; "171"; "172"; "173"; "174"; "175"; "176"; "177"; "178"; "179"; "180"; "181"; "182"; "183"; "184"; "185"; "186"; "187"; "188"; "189"; "190"; "191"; "192"; "193"; "194"; "195"; "196"; "197"; "198"; "199"; "200"; "201"; "202"; "203"; "204"; "205"; "206"; "207"; "208"; "209"; "210"; "211"; "212"; "213"; "214"; "215"; "216"; "217"; "218"; "219"; "220"; "221"; "222"; "223"; "224"; "225"; "226"; "227"; "228"; "229"; "230"; "231"; "232"; "233"; "234"; "235"; "236"; "237"; "238"; "239"; "240"; "241"; "242"; "243"; "244"; "245"; "246"; "247"; "248"; "249"; "250"; "251"; "252"; "253"; "254"; "255"]
+     : list byte
+     = ["000"; "001"; "002"; "003"; "004"; "005"; "006"; "007"; "008"; "009"; "010"; "011"; "012"; "013"; "014"; "015"; "016"; "017"; "018"; "019"; "020"; "021"; "022"; "023"; "024"; "025"; "026"; "027"; "028"; "029"; "030"; "031"; " "; "!"; """"; "#"; "$"; "%"; "&"; "'"; "("; ")"; "*"; "+"; ","; "-"; "."; "/"; "0"; "1"; "2"; "3"; "4"; "5"; "6"; "7"; "8"; "9"; ":"; ";"; "<"; "="; ">"; "?"; "@"; "A"; "B"; "C"; "D"; "E"; "F"; "G"; "H"; "I"; "J"; "K"; "L"; "M"; "N"; "O"; "P"; "Q"; "R"; "S"; "T"; "U"; "V"; "W"; "X"; "Y"; "Z"; "["; "\"; "]"; "^"; "_"; "`"; "a"; "b"; "c"; "d"; "e"; "f"; "g"; "h"; "i"; "j"; "k"; "l"; "m"; "n"; "o"; "p"; "q"; "r"; "s"; "t"; "u"; "v"; "w"; "x"; "y"; "z"; "{"; "|"; "}"; "~"; "127"; "128"; "129"; "130"; "131"; "132"; "133"; "134"; "135"; "136"; "137"; "138"; "139"; "140"; "141"; "142"; "143"; "144"; "145"; "146"; "147"; "148"; "149"; "150"; "151"; "152"; "153"; "154"; "155"; "156"; "157"; "158"; "159"; "160"; "161"; "162"; "163"; "164"; "165"; "166"; "167";
+       "168"; "169"; "170"; "171"; "172"; "173"; "174"; "175"; "176"; "177"; "178"; "179"; "180"; "181"; "182"; "183"; "184"; "185"; "186"; "187"; "188"; "189"; "190"; "191"; "192"; "193"; "194"; "195"; "196"; "197"; "198"; "199"; "200"; "201"; "202"; "203"; "204"; "205"; "206"; "207"; "208"; "209"; "210"; "211"; "212"; "213"; "214"; "215"; "216"; "217"; "218"; "219"; "220"; "221"; "222"; "223"; "224"; "225"; "226"; "227"; "228"; "229"; "230"; "231"; "232"; "233"; "234"; "235"; "236"; "237"; "238"; "239"; "240"; "241"; "242"; "243"; "244"; "245"; "246"; "247"; "248"; "249"; "250"; "251"; "252"; "253"; "254"; "255"]
+     : list ascii
diff --git a/test-suite/output/StringSyntax.v b/test-suite/output/StringSyntax.v
new file mode 100644
index 0000000000..aab6e0bb03
--- /dev/null
+++ b/test-suite/output/StringSyntax.v
@@ -0,0 +1,52 @@
+Require Import Coq.Lists.List.
+Require Import Coq.Strings.String Coq.Strings.Byte Coq.Strings.Ascii.
+Import ListNotations.
+
+Set Printing Depth 100000.
+Set Printing Width 1000.
+
+Close Scope char_scope.
+Close Scope string_scope.
+
+Open Scope byte_scope.
+Print byte_rect.
+Print byte_rec.
+Print byte_ind.
+Check "000".
+Check "a".
+Check "127".
+Fail Check "€".
+Close Scope byte_scope.
+
+Open Scope char_scope.
+Check "000".
+Check "a".
+Check "127".
+Fail Check "€".
+Close Scope char_scope.
+
+Open Scope string_scope.
+Check "000".
+Check "a".
+Check "127".
+Check "€".
+Check String "001" EmptyString.
+Close Scope string_scope.
+
+Compute ascii_of_byte "a".
+Compute byte_of_ascii "a".
+Compute string_of_list_byte ("a"::nil)%byte.
+Compute list_byte_of_string "a".
+
+Local Open Scope byte_scope.
+Compute List.fold_right
+        (fun n ls => match Byte.of_nat n with
+                     | Some b => cons b ls
+                     | None => ls
+                     end)
+        nil
+        (List.seq 0 256).
+Local Close Scope byte_scope.
+Local Open Scope char_scope.
+Compute List.map Ascii.ascii_of_nat (List.seq 0 256).
+Local Close Scope char_scope.