🧱 Block_payload_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Definition hash_value
(predecessor_hash : Block_hash.t) (payload_round : Round_repr.t)
(operations : list Operation_list_hash.elt) : Block_payload_hash.t :=
let operations_hash := Operation_list_hash.compute operations in
let predecessor :=
Data_encoding.Binary.to_bytes_exn None Block_hash.encoding predecessor_hash
in
let round :=
Data_encoding.Binary.to_bytes_exn None Round_repr.encoding payload_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 ].
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Block_payload_hash.
Require TezosOfOCaml.Proto_alpha.Round_repr.
Definition hash_value
(predecessor_hash : Block_hash.t) (payload_round : Round_repr.t)
(operations : list Operation_list_hash.elt) : Block_payload_hash.t :=
let operations_hash := Operation_list_hash.compute operations in
let predecessor :=
Data_encoding.Binary.to_bytes_exn None Block_hash.encoding predecessor_hash
in
let round :=
Data_encoding.Binary.to_bytes_exn None Round_repr.encoding payload_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 ].