Skip to main content

🐆 Tx_rollup_withdraw_list_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.Path_encoding.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_prefixes.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_withdraw_repr.

Definition prefix : string :=
  Tx_rollup_prefixes.withdraw_list_hash.(Tx_rollup_prefixes.t.b58check_prefix).

Definition H :=
  Blake2B.Make
    {|
      Blake2B.Register.register_encoding _ := Base58.register_encoding
    |}
    (let name := "Withdraw_list_hash" in
    let title := "A list of withdraw orders" in
    let b58check_prefix := prefix in
    let size_value :=
      Some
        Tx_rollup_prefixes.withdraw_list_hash.(Tx_rollup_prefixes.t.hash_size)
      in
    {|
      Blake2B.PrefixedName.name := name;
      Blake2B.PrefixedName.title := title;
      Blake2B.PrefixedName.size_value := size_value;
      Blake2B.PrefixedName.b58check_prefix := b58check_prefix
    |}).

Inclusion of the module [H]
Definition t := H.(S.HASH.t).

Definition name := H.(S.HASH.name).

Definition title := H.(S.HASH.title).

Definition pp := H.(S.HASH.pp).

Definition pp_short := H.(S.HASH.pp_short).

Definition op_eq := H.(S.HASH.op_eq).

Definition op_ltgt := H.(S.HASH.op_ltgt).

Definition op_lt := H.(S.HASH.op_lt).

Definition op_lteq := H.(S.HASH.op_lteq).

Definition op_gteq := H.(S.HASH.op_gteq).

Definition op_gt := H.(S.HASH.op_gt).

Definition compare := H.(S.HASH.compare).

Definition equal := H.(S.HASH.equal).

Definition max := H.(S.HASH.max).

Definition min := H.(S.HASH.min).

Definition hash_bytes := H.(S.HASH.hash_bytes).

Definition hash_string := H.(S.HASH.hash_string).

Definition zero := H.(S.HASH.zero).

Definition size_value := H.(S.HASH.size_value).

Definition to_bytes := H.(S.HASH.to_bytes).

Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).

Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).

Definition to_b58check := H.(S.HASH.to_b58check).

Definition to_short_b58check := H.(S.HASH.to_short_b58check).

Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).

Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).

Definition b58check_encoding := H.(S.HASH.b58check_encoding).

Definition encoding := H.(S.HASH.encoding).

Definition rpc_arg := H.(S.HASH.rpc_arg).

Definition Path_encoding_Make_hex_include :=
  Path_encoding.Make_hex
    {|
      Path_encoding.ENCODING.to_bytes := H.(S.HASH.to_bytes);
      Path_encoding.ENCODING.of_bytes_opt := H.(S.HASH.of_bytes_opt)
    |}.

Inclusion of the module [Path_encoding_Make_hex_include]
Init function; without side-effects in Coq