Skip to main content

🎫 Ticket_hash_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Script_expr_hash.
Require TezosOfOCaml.Proto_alpha.Storage_description.

Definition t : Set := Script_expr_hash.t.

Definition encoding : Data_encoding.t Script_expr_hash.t :=
  Script_expr_hash.encoding.

Definition pp : Format.formatter Script_expr_hash.t unit :=
  Script_expr_hash.pp.

Definition to_b58check : Script_expr_hash.t string :=
  Script_expr_hash.to_b58check.

Definition of_b58check_opt : string option Script_expr_hash.t :=
  Script_expr_hash.of_b58check_opt.

Definition of_b58check_exn : string Script_expr_hash.t :=
  Script_expr_hash.of_b58check_exn.

Definition of_bytes_exn : bytes Script_expr_hash.t :=
  Script_expr_hash.of_bytes_exn.

Definition of_bytes_opt : bytes option Script_expr_hash.t :=
  Script_expr_hash.of_bytes_opt.

Definition Compare_Make_include :=
  Compare.Make
    (let t : Set := Script_expr_hash.t in
    let compare := Script_expr_hash.compare in
    {|
      Compare.COMPARABLE.compare := compare
    |}).

Inclusion of the module [Compare_Make_include]