🐆 Tx_rollup_l2_context_hash.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Definition Blake2B_Make_include :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "tx_rollup_context_hash" in
let title := "Hash of a transaction rollup context" in
let b58check_prefix :=
String.String "017" (String.String "143" (String.String "019" "")) in
let size_value := Some 32 in
{|
Blake2B.PrefixedName.name := name;
Blake2B.PrefixedName.title := title;
Blake2B.PrefixedName.size_value := size_value;
Blake2B.PrefixedName.b58check_prefix := b58check_prefix
|}).
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Definition Blake2B_Make_include :=
Blake2B.Make
{|
Blake2B.Register.register_encoding _ := Base58.register_encoding
|}
(let name := "tx_rollup_context_hash" in
let title := "Hash of a transaction rollup context" in
let b58check_prefix :=
String.String "017" (String.String "143" (String.String "019" "")) in
let size_value := Some 32 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 [Blake2B_Make_include]
Definition t := Blake2B_Make_include.(S.HASH.t).
Definition name := Blake2B_Make_include.(S.HASH.name).
Definition title := Blake2B_Make_include.(S.HASH.title).
Definition pp := Blake2B_Make_include.(S.HASH.pp).
Definition pp_short := Blake2B_Make_include.(S.HASH.pp_short).
Definition op_eq := Blake2B_Make_include.(S.HASH.op_eq).
Definition op_ltgt := Blake2B_Make_include.(S.HASH.op_ltgt).
Definition op_lt := Blake2B_Make_include.(S.HASH.op_lt).
Definition op_lteq := Blake2B_Make_include.(S.HASH.op_lteq).
Definition op_gteq := Blake2B_Make_include.(S.HASH.op_gteq).
Definition op_gt := Blake2B_Make_include.(S.HASH.op_gt).
Definition compare := Blake2B_Make_include.(S.HASH.compare).
Definition equal := Blake2B_Make_include.(S.HASH.equal).
Definition max := Blake2B_Make_include.(S.HASH.max).
Definition min := Blake2B_Make_include.(S.HASH.min).
Definition hash_bytes := Blake2B_Make_include.(S.HASH.hash_bytes).
Definition hash_string := Blake2B_Make_include.(S.HASH.hash_string).
Definition zero := Blake2B_Make_include.(S.HASH.zero).
Definition size_value := Blake2B_Make_include.(S.HASH.size_value).
Definition to_bytes := Blake2B_Make_include.(S.HASH.to_bytes).
Definition of_bytes_opt := Blake2B_Make_include.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := Blake2B_Make_include.(S.HASH.of_bytes_exn).
Definition to_b58check := Blake2B_Make_include.(S.HASH.to_b58check).
Definition to_short_b58check := Blake2B_Make_include.(S.HASH.to_short_b58check).
Definition of_b58check_exn := Blake2B_Make_include.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := Blake2B_Make_include.(S.HASH.of_b58check_opt).
Definition b58check_encoding := Blake2B_Make_include.(S.HASH.b58check_encoding).
Definition encoding := Blake2B_Make_include.(S.HASH.encoding).
Definition rpc_arg := Blake2B_Make_include.(S.HASH.rpc_arg).
Definition name := Blake2B_Make_include.(S.HASH.name).
Definition title := Blake2B_Make_include.(S.HASH.title).
Definition pp := Blake2B_Make_include.(S.HASH.pp).
Definition pp_short := Blake2B_Make_include.(S.HASH.pp_short).
Definition op_eq := Blake2B_Make_include.(S.HASH.op_eq).
Definition op_ltgt := Blake2B_Make_include.(S.HASH.op_ltgt).
Definition op_lt := Blake2B_Make_include.(S.HASH.op_lt).
Definition op_lteq := Blake2B_Make_include.(S.HASH.op_lteq).
Definition op_gteq := Blake2B_Make_include.(S.HASH.op_gteq).
Definition op_gt := Blake2B_Make_include.(S.HASH.op_gt).
Definition compare := Blake2B_Make_include.(S.HASH.compare).
Definition equal := Blake2B_Make_include.(S.HASH.equal).
Definition max := Blake2B_Make_include.(S.HASH.max).
Definition min := Blake2B_Make_include.(S.HASH.min).
Definition hash_bytes := Blake2B_Make_include.(S.HASH.hash_bytes).
Definition hash_string := Blake2B_Make_include.(S.HASH.hash_string).
Definition zero := Blake2B_Make_include.(S.HASH.zero).
Definition size_value := Blake2B_Make_include.(S.HASH.size_value).
Definition to_bytes := Blake2B_Make_include.(S.HASH.to_bytes).
Definition of_bytes_opt := Blake2B_Make_include.(S.HASH.of_bytes_opt).
Definition of_bytes_exn := Blake2B_Make_include.(S.HASH.of_bytes_exn).
Definition to_b58check := Blake2B_Make_include.(S.HASH.to_b58check).
Definition to_short_b58check := Blake2B_Make_include.(S.HASH.to_short_b58check).
Definition of_b58check_exn := Blake2B_Make_include.(S.HASH.of_b58check_exn).
Definition of_b58check_opt := Blake2B_Make_include.(S.HASH.of_b58check_opt).
Definition b58check_encoding := Blake2B_Make_include.(S.HASH.b58check_encoding).
Definition encoding := Blake2B_Make_include.(S.HASH.encoding).
Definition rpc_arg := Blake2B_Make_include.(S.HASH.rpc_arg).
Init function; without side-effects in Coq