Skip to main content

🐆 Tx_rollup_l2_address.v

Translated OCaml

See proofs, 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.Cache_memory_helpers.
Require TezosOfOCaml.Proto_alpha.Indexable.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_prefixes.

Definition Blake2B_Make_include :=
  Blake2B.Make
    {|
      Blake2B.Register.register_encoding _ := Base58.register_encoding
    |}
    (let name := "Tx_rollup_l2_address" in
    let title :=
      "The hash of a BLS public key used to identify a L2 ticket holders" in
    let b58check_prefix :=
      Tx_rollup_prefixes.l2_address.(Tx_rollup_prefixes.t.b58check_prefix) in
    let size_value :=
      Some Tx_rollup_prefixes.l2_address.(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 [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 Compare_Make_include :=
  Compare.Make
    (let t : Set := t in
    {|
      Compare.COMPARABLE.compare := Blake2B_Make_include.(S.HASH.compare)
    |}).

Inclusion of the module [Compare_Make_include]
Init function; without side-effects in Coq
Inclusion of the module [Indexable_Make_include]
  Definition t := Indexable_Make_include.(Indexable.INDEXABLE.t).

  Definition index := Indexable_Make_include.(Indexable.INDEXABLE.index).

  Definition value := Indexable_Make_include.(Indexable.INDEXABLE.value).

  Definition either := Indexable_Make_include.(Indexable.INDEXABLE.either).

  Definition value_value :=
    Indexable_Make_include.(Indexable.INDEXABLE.value_value).

  Definition index_value :=
    Indexable_Make_include.(Indexable.INDEXABLE.index_value).

  Definition index_exn :=
    Indexable_Make_include.(Indexable.INDEXABLE.index_exn).

  Definition compact := Indexable_Make_include.(Indexable.INDEXABLE.compact).

  Definition encoding := Indexable_Make_include.(Indexable.INDEXABLE.encoding).

  Definition index_encoding :=
    Indexable_Make_include.(Indexable.INDEXABLE.index_encoding).

  Definition value_encoding :=
    Indexable_Make_include.(Indexable.INDEXABLE.value_encoding).

  Definition compare :=
    Indexable_Make_include.(Indexable.INDEXABLE.compare)
      .

  Definition compare_values :=
    Indexable_Make_include.(Indexable.INDEXABLE.compare_values).

  Definition compare_indexes :=
    Indexable_Make_include.(Indexable.INDEXABLE.compare_indexes).

  Definition pp {state : Set} :=
    Indexable_Make_include.(Indexable.INDEXABLE.pp) .

  Definition in_memory_size (x_value : Indexable.t)
    : Cache_memory_helpers.sint :=
    Indexable.in_memory_size in_memory_size x_value.

  Definition size_value (x_value : Indexable.t) : int :=
    Indexable.size_value size_value x_value.
End Indexable.