🍃 Char.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Definition code : ascii → int :=
fun c ⇒
Z.of_N (Ascii.N_of_ascii c).
Definition chr : int → ascii :=
fun z ⇒
Ascii.ascii_of_N (Z.to_N z).
Parameter escaped : ascii → string.
Definition lowercase_ascii(c : ascii) : ascii :=
let n := code c in
(* 65="A" *) (* 90="Z" *)
if ((65 <=? n) && (n <=? 90))%bool then chr (n + 32)%Z else c.
Definition uppercase_ascii(c : ascii) : ascii :=
let n := code c in
(* 97="a" *) (* 122="z" *)
if ((97 <=? n) && (n <=? 122))%bool then chr (n - 32)%Z else c.
Definition t : Set := ascii.
Definition compare : t → t → int :=
fun x y ⇒
Z.sub (code x) (code y).
Definition equal : t → t → bool :=
Ascii.eqb.
Require Import CoqOfOCaml.Settings.
Definition code : ascii → int :=
fun c ⇒
Z.of_N (Ascii.N_of_ascii c).
Definition chr : int → ascii :=
fun z ⇒
Ascii.ascii_of_N (Z.to_N z).
Parameter escaped : ascii → string.
Definition lowercase_ascii(c : ascii) : ascii :=
let n := code c in
(* 65="A" *) (* 90="Z" *)
if ((65 <=? n) && (n <=? 90))%bool then chr (n + 32)%Z else c.
Definition uppercase_ascii(c : ascii) : ascii :=
let n := code c in
(* 97="a" *) (* 122="z" *)
if ((97 <=? n) && (n <=? 122))%bool then chr (n - 32)%Z else c.
Definition t : Set := ascii.
Definition compare : t → t → int :=
fun x y ⇒
Z.sub (code x) (code y).
Definition equal : t → t → bool :=
Ascii.eqb.