🔡 Non_empty_string.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Proto_alpha.Non_empty_string.

Require TezosOfOCaml.Environment.V8.Proofs.Compare.

Module Valid.
  Definition t (s : string) : Prop :=
    s ≠ "".
End Valid.

Lemma compare_is_valid :
  Compare.Valid.t (fun _ ⇒ True) id Non_empty_string.compare.
Proof.
  apply Compare.string_is_valid.
Qed.

Lemma of_string_is_valid s :
  match Non_empty_string.of_string s with
  | Some s ⇒ Valid.t s
  | None ⇒ True
  end.
  now destruct s.
Qed.

Lemma of_string_eq s :
  Valid.t s →
  Non_empty_string.of_string s = Some s.
  now destruct s.
Qed.

Lemma of_string_exn_eq s :
  Valid.t s →
  Non_empty_string.of_string_exn s = s.
  now destruct s.
Qed.