🍃 Hex.v

Proofs

See code, Gitlab

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

Require Import TezosOfOCaml.Environment.V8.

Axiom of_bytes_to_bytes : ∀ h,
  match Hex.to_bytes h with
  | Some b ⇒ Hex.of_bytes None b = h
  | None ⇒ True
  end.

Axiom to_bytes_of_bytes : ∀ h, Hex.to_bytes (Hex.of_bytes None h) = Some h.