👔 Manager_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.

Inductive manager_key : Set :=
| Hash : Signature.public_key_hash → manager_key
| Public_key : Signature.public_key → manager_key.

Definition t : Set := manager_key.

Definition hash_case (tag : Data_encoding.case_tag)
  : Data_encoding.case manager_key :=
  Data_encoding.case_value "Public_key_hash" None tag
    Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.encoding)
    (fun (function_parameter : manager_key) ⇒
      match function_parameter with
      | Hash hash_value ⇒ Some hash_value
      | _ ⇒ None
      end) (fun (hash_value : Signature.public_key_hash) ⇒ Hash hash_value).

Definition pubkey_case (tag : Data_encoding.case_tag)
  : Data_encoding.case manager_key :=
  Data_encoding.case_value "Public_key" None tag
    Signature.Public_key.(S.SIGNATURE_PUBLIC_KEY.encoding)
    (fun (function_parameter : manager_key) ⇒
      match function_parameter with
      | Public_key hash_value ⇒ Some hash_value
      | _ ⇒ None
      end) (fun (hash_value : Signature.public_key) ⇒ Public_key hash_value).

Definition encoding : Data_encoding.encoding manager_key :=
  Data_encoding.union None
    [ hash_case (Data_encoding.Tag 0); pubkey_case (Data_encoding.Tag 1) ].