aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/StringSyntax.v
diff options
context:
space:
mode:
authorJason Gross2018-11-28 15:20:32 -0500
committerJason Gross2018-11-28 15:20:32 -0500
commitcac9811632834b0135f4408a32b4a2d391d09a0d (patch)
treed556b22c660898e89531bb43093ea0c8238da24e /test-suite/output/StringSyntax.v
parentf5e3d9e29f030a86433bb2700e55c4c183593163 (diff)
Add a couple more printing tests for byte/ascii
Diffstat (limited to 'test-suite/output/StringSyntax.v')
-rw-r--r--test-suite/output/StringSyntax.v13
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/output/StringSyntax.v b/test-suite/output/StringSyntax.v
index 477a4dd1c6..aab6e0bb03 100644
--- a/test-suite/output/StringSyntax.v
+++ b/test-suite/output/StringSyntax.v
@@ -37,3 +37,16 @@ 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.