🍃 Context_hash.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Compare.
Require TezosOfOCaml.Environment.Structs.V0.S.
Parameter Included_HASH_t : Set.
Parameter Included_HASH_Set_t : Set.
Parameter Included_HASH_Map_t : Set → Set.
Parameter Included_HASH :
S.HASH (t := Included_HASH_t) (Set_t := Included_HASH_Set_t)
(Map_t := Included_HASH_Map_t).
Definition t := Included_HASH.(S.HASH.t).
Definition name : string := Included_HASH.(S.HASH.name).
Definition title : string := Included_HASH.(S.HASH.title).
Definition pp : Format.formatter → t → unit := Included_HASH.(S.HASH.pp).
Definition pp_short : Format.formatter → t → unit :=
Included_HASH.(S.HASH.pp_short).
Definition op_eq : t → t → bool := Included_HASH.(S.HASH.op_eq).
Definition op_ltgt : t → t → bool := Included_HASH.(S.HASH.op_ltgt).
Definition op_lt : t → t → bool := Included_HASH.(S.HASH.op_lt).
Definition op_lteq : t → t → bool := Included_HASH.(S.HASH.op_lteq).
Definition op_gteq : t → t → bool := Included_HASH.(S.HASH.op_gteq).
Definition op_gt : t → t → bool := Included_HASH.(S.HASH.op_gt).
Definition compare : t → t → int := Included_HASH.(S.HASH.compare).
Definition equal : t → t → bool := Included_HASH.(S.HASH.equal).
Definition max : t → t → t := Included_HASH.(S.HASH.max).
Definition min : t → t → t := Included_HASH.(S.HASH.min).
Definition hash_bytes : option bytes → list bytes → t :=
Included_HASH.(S.HASH.hash_bytes).
Definition hash_string : option string → list string → t :=
Included_HASH.(S.HASH.hash_string).
Definition zero : t := Included_HASH.(S.HASH.zero).
Definition size_value : int := Included_HASH.(S.HASH.size_value).
Definition to_bytes : t → bytes := Included_HASH.(S.HASH.to_bytes).
Definition of_bytes_opt : bytes → option t :=
Included_HASH.(S.HASH.of_bytes_opt).
Definition of_bytes_exn : bytes → t := Included_HASH.(S.HASH.of_bytes_exn).
Definition to_b58check : t → string := Included_HASH.(S.HASH.to_b58check).
Definition to_short_b58check : t → string :=
Included_HASH.(S.HASH.to_short_b58check).
Definition of_b58check_exn : string → t :=
Included_HASH.(S.HASH.of_b58check_exn).
Definition of_b58check_opt : string → option t :=
Included_HASH.(S.HASH.of_b58check_opt).
Definition b58check_encoding : Base58.encoding t :=
Included_HASH.(S.HASH.b58check_encoding).
Definition encoding : Data_encoding.t t := Included_HASH.(S.HASH.encoding).
Definition rpc_arg : RPC_arg.t t := Included_HASH.(S.HASH.rpc_arg).
Definition _Set := Included_HASH.(S.HASH._Set).
Definition Map := Included_HASH.(S.HASH.Map).
Module Version.
Definition t : Set := int.
Parameter Included_S : Compare.S (t := t).
Definition op_eq : t → t → bool := Included_S.(Compare.S.op_eq).
Definition op_ltgt : t → t → bool := Included_S.(Compare.S.op_ltgt).
Definition op_lt : t → t → bool := Included_S.(Compare.S.op_lt).
Definition op_lteq : t → t → bool := Included_S.(Compare.S.op_lteq).
Definition op_gteq : t → t → bool := Included_S.(Compare.S.op_gteq).
Definition op_gt : t → t → bool := Included_S.(Compare.S.op_gt).
Definition compare : t → t → int := Included_S.(Compare.S.compare).
Definition equal : t → t → bool := Included_S.(Compare.S.equal).
Definition max : t → t → t := Included_S.(Compare.S.max).
Definition min : t → t → t := Included_S.(Compare.S.min).
Parameter pp : Format.formatter → t → unit.
Parameter encoding : Data_encoding.t t.
Parameter of_int : int → t.
End Version.
Definition version : Set := Version.t.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Compare.
Require TezosOfOCaml.Environment.Structs.V0.S.
Parameter Included_HASH_t : Set.
Parameter Included_HASH_Set_t : Set.
Parameter Included_HASH_Map_t : Set → Set.
Parameter Included_HASH :
S.HASH (t := Included_HASH_t) (Set_t := Included_HASH_Set_t)
(Map_t := Included_HASH_Map_t).
Definition t := Included_HASH.(S.HASH.t).
Definition name : string := Included_HASH.(S.HASH.name).
Definition title : string := Included_HASH.(S.HASH.title).
Definition pp : Format.formatter → t → unit := Included_HASH.(S.HASH.pp).
Definition pp_short : Format.formatter → t → unit :=
Included_HASH.(S.HASH.pp_short).
Definition op_eq : t → t → bool := Included_HASH.(S.HASH.op_eq).
Definition op_ltgt : t → t → bool := Included_HASH.(S.HASH.op_ltgt).
Definition op_lt : t → t → bool := Included_HASH.(S.HASH.op_lt).
Definition op_lteq : t → t → bool := Included_HASH.(S.HASH.op_lteq).
Definition op_gteq : t → t → bool := Included_HASH.(S.HASH.op_gteq).
Definition op_gt : t → t → bool := Included_HASH.(S.HASH.op_gt).
Definition compare : t → t → int := Included_HASH.(S.HASH.compare).
Definition equal : t → t → bool := Included_HASH.(S.HASH.equal).
Definition max : t → t → t := Included_HASH.(S.HASH.max).
Definition min : t → t → t := Included_HASH.(S.HASH.min).
Definition hash_bytes : option bytes → list bytes → t :=
Included_HASH.(S.HASH.hash_bytes).
Definition hash_string : option string → list string → t :=
Included_HASH.(S.HASH.hash_string).
Definition zero : t := Included_HASH.(S.HASH.zero).
Definition size_value : int := Included_HASH.(S.HASH.size_value).
Definition to_bytes : t → bytes := Included_HASH.(S.HASH.to_bytes).
Definition of_bytes_opt : bytes → option t :=
Included_HASH.(S.HASH.of_bytes_opt).
Definition of_bytes_exn : bytes → t := Included_HASH.(S.HASH.of_bytes_exn).
Definition to_b58check : t → string := Included_HASH.(S.HASH.to_b58check).
Definition to_short_b58check : t → string :=
Included_HASH.(S.HASH.to_short_b58check).
Definition of_b58check_exn : string → t :=
Included_HASH.(S.HASH.of_b58check_exn).
Definition of_b58check_opt : string → option t :=
Included_HASH.(S.HASH.of_b58check_opt).
Definition b58check_encoding : Base58.encoding t :=
Included_HASH.(S.HASH.b58check_encoding).
Definition encoding : Data_encoding.t t := Included_HASH.(S.HASH.encoding).
Definition rpc_arg : RPC_arg.t t := Included_HASH.(S.HASH.rpc_arg).
Definition _Set := Included_HASH.(S.HASH._Set).
Definition Map := Included_HASH.(S.HASH.Map).
Module Version.
Definition t : Set := int.
Parameter Included_S : Compare.S (t := t).
Definition op_eq : t → t → bool := Included_S.(Compare.S.op_eq).
Definition op_ltgt : t → t → bool := Included_S.(Compare.S.op_ltgt).
Definition op_lt : t → t → bool := Included_S.(Compare.S.op_lt).
Definition op_lteq : t → t → bool := Included_S.(Compare.S.op_lteq).
Definition op_gteq : t → t → bool := Included_S.(Compare.S.op_gteq).
Definition op_gt : t → t → bool := Included_S.(Compare.S.op_gt).
Definition compare : t → t → int := Included_S.(Compare.S.compare).
Definition equal : t → t → bool := Included_S.(Compare.S.equal).
Definition max : t → t → t := Included_S.(Compare.S.max).
Definition min : t → t → t := Included_S.(Compare.S.min).
Parameter pp : Format.formatter → t → unit.
Parameter encoding : Data_encoding.t t.
Parameter of_int : int → t.
End Version.
Definition version : Set := Version.t.