Skip to main content

🍃 Char.v

Environment

Gitlab , OCaml

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.