🍃 Q.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Format.
Module t.
Record record : Set := Build {
num : Z.t;
den : Z.t;
}.
Definition with_num num (r : record) :=
Build num r.(den).
Definition with_den den (r : record) :=
Build r.(num) den.
End t.
Definition t := t.record.
Parameter make : Z.t → Z.t → t.
Parameter zero : t.
Parameter one : t.
Parameter minus_one : t.
Parameter inf : t.
Parameter minus_inf : t.
Parameter undef : t.
Parameter of_bigint : Z.t → t.
Parameter of_int : int → t.
Parameter of_int32 : int32 → t.
Parameter of_int64 : int64 → t.
Parameter of_ints : int → int → t.
Parameter of_string : string → t.
Parameter num : t → Z.t.
Parameter den : t → Z.t.
Inductive kind : Set :=
| ZERO : kind
| INF : kind
| MINF : kind
| UNDEF : kind
| NZERO : kind.
Parameter classify : t → kind.
Parameter is_real : t → bool.
Parameter sign : t → int.
Parameter compare : t → t → int.
Parameter equal : t → t → bool.
Parameter min : t → t → t.
Parameter max : t → t → t.
Parameter leq : t → t → bool.
Parameter geq : t → t → bool.
Parameter lt : t → t → bool.
Parameter gt : t → t → bool.
Parameter to_bigint : t → Z.t.
Parameter to_int : t → int.
Parameter to_int32 : t → int32.
Parameter to_int64 : t → int64.
Parameter to_string : t → string.
Parameter neg : t → t.
Parameter abs : t → t.
Parameter add : t → t → t.
Parameter sub : t → t → t.
Parameter mul : t → t → t.
Parameter inv : t → t.
Parameter div : t → t → t.
Parameter mul_2exp : t → int → t.
Parameter div_2exp : t → int → t.
Parameter pp_print : Format.formatter → t → unit.
Parameter op_tildeminus : t → t.
Parameter op_tildeplus : t → t.
Parameter op_plus : t → t → t.
Parameter op_minus : t → t → t.
Parameter op_star : t → t → t.
Parameter op_div : t → t → t.
Parameter lsl : t → int → t.
Parameter asr : t → int → t.
Parameter op_tildedollar : int → t.
Parameter op_divdiv : int → int → t.
Parameter op_tildedollardollar : Z.t → t.
Parameter op_divdivdiv : Z.t → Z.t → t.
Parameter op_eq : t → t → bool.
Parameter op_lt : t → t → bool.
Parameter op_gt : t → t → bool.
Parameter op_lteq : t → t → bool.
Parameter op_gteq : t → t → bool.
Parameter op_ltgt : t → t → bool.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Format.
Module t.
Record record : Set := Build {
num : Z.t;
den : Z.t;
}.
Definition with_num num (r : record) :=
Build num r.(den).
Definition with_den den (r : record) :=
Build r.(num) den.
End t.
Definition t := t.record.
Parameter make : Z.t → Z.t → t.
Parameter zero : t.
Parameter one : t.
Parameter minus_one : t.
Parameter inf : t.
Parameter minus_inf : t.
Parameter undef : t.
Parameter of_bigint : Z.t → t.
Parameter of_int : int → t.
Parameter of_int32 : int32 → t.
Parameter of_int64 : int64 → t.
Parameter of_ints : int → int → t.
Parameter of_string : string → t.
Parameter num : t → Z.t.
Parameter den : t → Z.t.
Inductive kind : Set :=
| ZERO : kind
| INF : kind
| MINF : kind
| UNDEF : kind
| NZERO : kind.
Parameter classify : t → kind.
Parameter is_real : t → bool.
Parameter sign : t → int.
Parameter compare : t → t → int.
Parameter equal : t → t → bool.
Parameter min : t → t → t.
Parameter max : t → t → t.
Parameter leq : t → t → bool.
Parameter geq : t → t → bool.
Parameter lt : t → t → bool.
Parameter gt : t → t → bool.
Parameter to_bigint : t → Z.t.
Parameter to_int : t → int.
Parameter to_int32 : t → int32.
Parameter to_int64 : t → int64.
Parameter to_string : t → string.
Parameter neg : t → t.
Parameter abs : t → t.
Parameter add : t → t → t.
Parameter sub : t → t → t.
Parameter mul : t → t → t.
Parameter inv : t → t.
Parameter div : t → t → t.
Parameter mul_2exp : t → int → t.
Parameter div_2exp : t → int → t.
Parameter pp_print : Format.formatter → t → unit.
Parameter op_tildeminus : t → t.
Parameter op_tildeplus : t → t.
Parameter op_plus : t → t → t.
Parameter op_minus : t → t → t.
Parameter op_star : t → t → t.
Parameter op_div : t → t → t.
Parameter lsl : t → int → t.
Parameter asr : t → int → t.
Parameter op_tildedollar : int → t.
Parameter op_divdiv : int → int → t.
Parameter op_tildedollardollar : Z.t → t.
Parameter op_divdivdiv : Z.t → Z.t → t.
Parameter op_eq : t → t → bool.
Parameter op_lt : t → t → bool.
Parameter op_gt : t → t → bool.
Parameter op_lteq : t → t → bool.
Parameter op_gteq : t → t → bool.
Parameter op_ltgt : t → t → bool.