🧱 Block_payload_repr.v

Translated OCaml

Gitlab , OCaml

File generated by coq-of-ocaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Round_repr.

Definition hash_value
  (predecessor : Block_hash.t) (round : Round_repr.t)
  (operations_hash : Operation_list_hash.t) : Block_payload_hash.t :=
  let predecessor :=
    Data_encoding.Binary.to_bytes_exn None Block_hash.encoding predecessor in
  let round := Data_encoding.Binary.to_bytes_exn None Round_repr.encoding round
    in
  let operations_hash :=
    Data_encoding.Binary.to_bytes_exn None Operation_list_hash.encoding
      operations_hash in
  Block_payload_hash.hash_bytes None [ predecessor; round; operations_hash ].