➗ Ratio_repr.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Module t.
Record record : Set := Build {
numerator : int;
denominator : int;
}.
Definition with_numerator numerator (r : record) :=
Build numerator r.(denominator).
Definition with_denominator denominator (r : record) :=
Build r.(numerator) denominator.
End t.
Definition t := t.record.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv_with_guard
(fun (r_value : t) ⇒ (r_value.(t.numerator), r_value.(t.denominator)))
(fun (function_parameter : int × int) ⇒
let '(numerator, denominator) := function_parameter in
if denominator >i 0 then
return? {| t.numerator := numerator; t.denominator := denominator; |}
else
Pervasives.Error "The denominator must be greater than 0.") None
(Data_encoding.obj2
(Data_encoding.req None None "numerator" Data_encoding.uint16)
(Data_encoding.req None None "denominator" Data_encoding.uint16)).
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
let '{| t.numerator := numerator; t.denominator := denominator |} :=
function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal "/" % char
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format))) "%d/%d") numerator
denominator.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Module t.
Record record : Set := Build {
numerator : int;
denominator : int;
}.
Definition with_numerator numerator (r : record) :=
Build numerator r.(denominator).
Definition with_denominator denominator (r : record) :=
Build r.(numerator) denominator.
End t.
Definition t := t.record.
Definition encoding : Data_encoding.encoding t :=
Data_encoding.conv_with_guard
(fun (r_value : t) ⇒ (r_value.(t.numerator), r_value.(t.denominator)))
(fun (function_parameter : int × int) ⇒
let '(numerator, denominator) := function_parameter in
if denominator >i 0 then
return? {| t.numerator := numerator; t.denominator := denominator; |}
else
Pervasives.Error "The denominator must be greater than 0.") None
(Data_encoding.obj2
(Data_encoding.req None None "numerator" Data_encoding.uint16)
(Data_encoding.req None None "denominator" Data_encoding.uint16)).
Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
let '{| t.numerator := numerator; t.denominator := denominator |} :=
function_parameter in
Format.fprintf fmt
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
(CamlinternalFormatBasics.Char_literal "/" % char
(CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.No_precision
CamlinternalFormatBasics.End_of_format))) "%d/%d") numerator
denominator.