Library Coq.Strings.Ascii
Contributed by Laurent Théry (INRIA);
Adapted to Coq V8 by the Coq Development Team
Definition of ascii characters
Definition of ascii character as a 8 bits constructor
Definition of a decidable function that is effective
Definition ascii_dec :
forall a b :
ascii, {
a =
b} + {
a <>
b}.
Defined.
Conversion between natural numbers modulo 256 and ascii characters
Auxillary function that turns a positive into an ascii by
looking at the last n bits, ie z mod 2^n
Function that turns a positive into an ascii by
looking at the last 8 bits, ie a mod 8
Function that turns a Peano number into an ascii by converting it
to positive
The opposite function
Definition nat_of_ascii (
a :
ascii) :
nat :=
let (
a1,
a2,
a3,
a4,
a5,
a6,
a7,
a8) :=
a in
2 *
(2 *
(2 *
(2 *
(2 *
(2 *
(2 * (
if a8 then 1
else 0)
+ (
if a7 then 1
else 0))
+ (
if a6 then 1
else 0))
+ (
if a5 then 1
else 0))
+ (
if a4 then 1
else 0))
+ (
if a3 then 1
else 0))
+ (
if a2 then 1
else 0))
+ (
if a1 then 1
else 0).
Theorem ascii_nat_embedding :
forall a :
ascii,
ascii_of_nat (
nat_of_ascii a) =
a.
Ascii characters can be represented in scope char_scope as follows:
- "c" represents itself if c is a character of code < 128,
- """" is an exception: it represents the ascii character 34
(double quote),
- "nnn" represents the ascii character of decimal code nnn.
For instance, both
"065" and
"A" denote the character `uppercase
A', and both
"034" and
"""" denote the character `double quote'.
Notice that the ascii characters of code >= 128 do not denote
stand-alone utf8 characters so that only the notation "nnn" is
available for them (unless your terminal is able to represent them,
which is typically not the case in coqide).
Open Local Scope char_scope.
Example Space := " ".
Example DoubleQuote := """".
Example Beep := "007".