🎫 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.Environment.V8.
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]

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

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

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

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

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

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

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

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

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

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

Definition zero : Script_expr_hash.t := Script_expr_hash.zero.

Definition of_script_expr_hash {A : Set} (t_value : A) : A := t_value.

Module Index.
  Include Script_expr_hash.

  (* Index *)
  Definition module :=
    {|
      Storage_description.INDEX.to_path := to_path;
      Storage_description.INDEX.of_path := of_path;
      Storage_description.INDEX.path_length := path_length;
      Storage_description.INDEX.rpc_arg := rpc_arg;
      Storage_description.INDEX.encoding := encoding;
      Storage_description.INDEX.compare := compare
    |}.
End Index.
Definition Index : Storage_description.INDEX (t := Script_expr_hash.t) :=
  Index.module.