🗳️ Vote_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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).
Definition equal_ballot (a_value : ballot) (b_value : ballot) : bool :=
match (a_value, b_value) with
| ((Yay, Yay) | (Nay, Nay) | (Pass, Pass)) ⇒ true
| _ ⇒ false
end.
Definition pp_ballot (ppf : Format.formatter) (function_parameter : ballot)
: unit :=
match function_parameter with
| Yay ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "yay"
CamlinternalFormatBasics.End_of_format) "yay")
| Nay ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "nay"
CamlinternalFormatBasics.End_of_format) "nay")
| Pass ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "pass"
CamlinternalFormatBasics.End_of_format) "pass")
end.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
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).
Definition equal_ballot (a_value : ballot) (b_value : ballot) : bool :=
match (a_value, b_value) with
| ((Yay, Yay) | (Nay, Nay) | (Pass, Pass)) ⇒ true
| _ ⇒ false
end.
Definition pp_ballot (ppf : Format.formatter) (function_parameter : ballot)
: unit :=
match function_parameter with
| Yay ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "yay"
CamlinternalFormatBasics.End_of_format) "yay")
| Nay ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "nay"
CamlinternalFormatBasics.End_of_format) "nay")
| Pass ⇒
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String_literal "pass"
CamlinternalFormatBasics.End_of_format) "pass")
end.