🍃 Operation_list_list_hash.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Operation_list_hash.
Require TezosOfOCaml.Environment.Structs.V0.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).
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Operation_list_hash.
Require TezosOfOCaml.Environment.Structs.V0.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).