🔡 Non_empty_string.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.

Inclusion of the module [Compare.String]

Definition t := Compare.String.(Compare.S.t).

Definition op_eq := Compare.String.(Compare.S.op_eq).

Definition op_ltgt := Compare.String.(Compare.S.op_ltgt).

Definition op_lt := Compare.String.(Compare.S.op_lt).

Definition op_lteq := Compare.String.(Compare.S.op_lteq).

Definition op_gteq := Compare.String.(Compare.S.op_gteq).

Definition op_gt := Compare.String.(Compare.S.op_gt).

Definition compare := Compare.String.(Compare.S.compare).

Definition equal := Compare.String.(Compare.S.equal).

Definition max := Compare.String.(Compare.S.max).

Definition min := Compare.String.(Compare.S.min).

Definition of_string (function_parameter : string) : option string :=
  match function_parameter with
  | "" ⇒ None
  | s_value ⇒ Some s_value
  end.

Definition of_string_exn (function_parameter : string) : string :=
  match function_parameter with
  | "" ⇒ Pervasives.invalid_arg "Unexpected empty string"
  | s_value ⇒ s_value
  end.

Definition cat2 (a_value : string) (op_staroptstar : option string)
  : string → string :=
  let sep :=
    match op_staroptstar with
    | Some op_starsthstar ⇒ op_starsthstar
    | None ⇒ ""
    end in
  fun (b_value : string) ⇒ String.concat sep [ a_value; b_value ].