Skip to main content

🍃 Operation_list_list_hash.v

Environment

See proofs, Gitlab , OCaml

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

Require Proto_alpha.Environment.Operation_list_hash.
Require Proto_alpha.Environment.S.

Parameter Included_MERKLE_TREE_t : Set.

Parameter Included_MERKLE_TREE_Set_t : Set.

Parameter Included_MERKLE_TREE_Map_t : Set Set.

Parameter Included_MERKLE_TREE_path : Set.

Parameter Included_MERKLE_TREE :
  S.MERKLE_TREE (elt := Operation_list_hash.t)
    (t := Included_MERKLE_TREE_t) (Set_t := Included_MERKLE_TREE_Set_t)
    (Map_t := Included_MERKLE_TREE_Map_t) (path := Included_MERKLE_TREE_path).

Definition elt := Included_MERKLE_TREE.(S.MERKLE_TREE.elt).

Definition t := Included_MERKLE_TREE.(S.MERKLE_TREE.t).

Definition name : string := Included_MERKLE_TREE.(S.MERKLE_TREE.name).

Definition title : string := Included_MERKLE_TREE.(S.MERKLE_TREE.title).

Definition pp : Format.formatter t unit :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.pp).

Definition pp_short : Format.formatter t unit :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.pp_short).

Definition op_eq : t t bool :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.op_eq).

Definition op_ltgt : t t bool :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.op_ltgt).

Definition op_lt : t t bool :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.op_lt).

Definition op_lteq : t t bool :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.op_lteq).

Definition op_gteq : t t bool :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.op_gteq).

Definition op_gt : t t bool :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.op_gt).

Definition compare : t t int :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.compare).

Definition equal : t t bool :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.equal).

Definition max : t t t := Included_MERKLE_TREE.(S.MERKLE_TREE.max).

Definition min : t t t := Included_MERKLE_TREE.(S.MERKLE_TREE.min).

Definition hash_bytes : option bytes list bytes t :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.hash_bytes).

Definition hash_string : option string list string t :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.hash_string).

Definition zero : t := Included_MERKLE_TREE.(S.MERKLE_TREE.zero).

Definition size_value : int := Included_MERKLE_TREE.(S.MERKLE_TREE.size_value).

Definition to_bytes : t bytes :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.to_bytes).

Definition of_bytes_opt : bytes option t :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.of_bytes_opt).

Definition of_bytes_exn : bytes t :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.of_bytes_exn).

Definition to_b58check : t string :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.to_b58check).

Definition to_short_b58check : t string :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.to_short_b58check).

Definition of_b58check_exn : string t :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.of_b58check_exn).

Definition of_b58check_opt : string option t :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.of_b58check_opt).

Definition b58check_encoding : Base58.encoding t :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.b58check_encoding).

Definition encoding : Data_encoding.t t :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.encoding).

Definition rpc_arg : RPC_arg.t t :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.rpc_arg).

Definition _Set := Included_MERKLE_TREE.(S.MERKLE_TREE._Set).

Definition Map := Included_MERKLE_TREE.(S.MERKLE_TREE.Map).

Definition compute : list elt t :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.compute).

Definition empty : t := Included_MERKLE_TREE.(S.MERKLE_TREE.empty).

Definition path := Included_MERKLE_TREE.(S.MERKLE_TREE.path).

Definition compute_path : list elt int path :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.compute_path).

Definition check_path : path elt t × int :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.check_path).

Definition path_encoding : Data_encoding.t path :=
  Included_MERKLE_TREE.(S.MERKLE_TREE.path_encoding).