aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Strings/Ascii.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2018-02-13 17:16:06 -0500
committerGravatar Jason Gross <jgross@mit.edu>2018-02-13 17:16:06 -0500
commit54a88659aedb098014cfc03ba3ca627647dfc665 (patch)
treef7ac7a753b6c106ade2e5a7b461940d4b57965bc /src/Util/Strings/Ascii.v
parentd704a3934f406c63a7d917fdb865ddf37e58d1e8 (diff)
Add some string utility functions
Diffstat (limited to 'src/Util/Strings/Ascii.v')
-rw-r--r--src/Util/Strings/Ascii.v15
1 files changed, 15 insertions, 0 deletions
diff --git a/src/Util/Strings/Ascii.v b/src/Util/Strings/Ascii.v
new file mode 100644
index 000000000..93ea9b749
--- /dev/null
+++ b/src/Util/Strings/Ascii.v
@@ -0,0 +1,15 @@
+Require Import Crypto.Util.Strings.Equality.
+Require Import Coq.Strings.Ascii.
+
+Local Open Scope char_scope.
+
+(** Special characters *)
+
+Example Null := "000".
+Example Backspace := "008".
+Example Tab := "009".
+Example LF := "010".
+Example NewPage := "012".
+Example CR := "013".
+Example Escape := "027".
+Example NewLine := "010".