Skip to main content

🗳️ Vote_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.Proto_alpha.Environment.

Definition proposal : Set := Protocol_hash.t.

Inductive ballot : Set :=
| Yay : ballot
| Nay : ballot
| Pass : ballot.

Definition ballot_encoding : Data_encoding.encoding ballot :=
  let of_int8 (function_parameter : int) : Pervasives.result ballot string :=
    match function_parameter with
    | 0 ⇒ Pervasives.Ok Yay
    | 1 ⇒ Pervasives.Ok Nay
    | 2 ⇒ Pervasives.Ok Pass
    | _Pervasives.Error "ballot_of_int8"
    end in
  let to_int8 (function_parameter : ballot) : int :=
    match function_parameter with
    | Yay ⇒ 0
    | Nay ⇒ 1
    | Pass ⇒ 2
    end in
  Data_encoding.splitted
    (Data_encoding.string_enum [ ("yay", Yay); ("nay", Nay); ("pass", Pass) ])
    (Data_encoding.conv_with_guard to_int8 of_int8 None Data_encoding.int8).