🍃 Hex.v
Proofs
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.
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.