💍 Commitment_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.Blinded_public_key_hash.
Require TezosOfOCaml.Proto_alpha.Tez_repr.

Module t.
  Record record : Set := Build {
    blinded_public_key_hash : Blinded_public_key_hash.t;
    amount : Tez_repr.t;
  }.
  Definition with_blinded_public_key_hash blinded_public_key_hash
    (r : record) :=
    Build blinded_public_key_hash r.(amount).
  Definition with_amount amount (r : record) :=
    Build r.(blinded_public_key_hash) amount.
End t.
Definition t := t.record.

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.conv
    (fun (function_parameter : t) ⇒
      let '{|
        t.blinded_public_key_hash := blinded_public_key_hash;
          t.amount := amount
          |} := function_parameter in
      (blinded_public_key_hash, amount))
    (fun (function_parameter : Blinded_public_key_hash.t × Tez_repr.t) ⇒
      let '(blinded_public_key_hash, amount) := function_parameter in
      {| t.blinded_public_key_hash := blinded_public_key_hash;
        t.amount := amount; |}) None
    (Data_encoding.tup2 Blinded_public_key_hash.encoding Tez_repr.encoding).