blob: aab6e0bb0335ef4a115fae68ec22acd41e2b5c5d (
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
|
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.
|
