From 02a9abde3e9b1e1ee92b65082b9da1e4ac12bf53 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 4 Jan 2022 11:11:30 -0500 Subject: [PATCH] feat: add Q.is_int --- src/arith/sidekick_arith.ml | 3 +++ src/zarith/sidekick_zarith.ml | 1 + 2 files changed, 4 insertions(+) diff --git a/src/arith/sidekick_arith.ml b/src/arith/sidekick_arith.ml index a6c11621..30514110 100644 --- a/src/arith/sidekick_arith.ml +++ b/src/arith/sidekick_arith.ml @@ -53,6 +53,9 @@ module type RATIONAL = sig val is_real : t -> bool (** A proper real, not nan/infinity *) + val is_int : t -> bool + (** Is this a proper integer? *) + val pp_approx : int -> Format.formatter -> t -> unit (** Pretty print rational with given amount of precision (for example as a floating point number) *) diff --git a/src/zarith/sidekick_zarith.ml b/src/zarith/sidekick_zarith.ml index a3260b96..93f7b826 100644 --- a/src/zarith/sidekick_zarith.ml +++ b/src/zarith/sidekick_zarith.ml @@ -18,6 +18,7 @@ module Rational let infinity = Q.inf let minus_infinity = Q.minus_inf let is_real = Q.is_real + let is_int q = is_real q && Z.(equal (denum q) one) let pp_approx n out q = Format.fprintf out "%*.1f" n (Q.to_float q) end