Skip to main content

🍃 Q.v

Environment

Gitlab

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.