diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /plugins/micromega/mutils.mli | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'plugins/micromega/mutils.mli')
-rw-r--r-- | plugins/micromega/mutils.mli | 70 |
1 files changed, 70 insertions, 0 deletions
diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli new file mode 100644 index 00000000..094429ea --- /dev/null +++ b/plugins/micromega/mutils.mli @@ -0,0 +1,70 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +val numerator : Num.num -> Big_int.big_int +val denominator : Num.num -> Big_int.big_int + +module Cmp : sig + + val compare_list : ('a -> 'b -> int) -> 'a list -> 'b list -> int + val compare_lexical : (unit -> int) list -> int + +end + +module Tag : sig + + type t + + val pp : out_channel -> t -> unit + val next : t -> t + val from : int -> t + +end + +module TagSet : CSig.SetS with type elt = Tag.t + +val pp_list : (out_channel -> 'a -> unit) -> out_channel -> 'a list -> unit + +module CamlToCoq : sig + + val positive : int -> Micromega.positive + val bigint : Big_int.big_int -> Micromega.z + val n : int -> Micromega.n + val nat : int -> Micromega.nat + val q : Num.num -> Micromega.q + val index : int -> Micromega.positive + val z : int -> Micromega.z + val positive_big_int : Big_int.big_int -> Micromega.positive + +end + +module CoqToCaml : sig + + val z_big_int : Micromega.z -> Big_int.big_int + val q_to_num : Micromega.q -> Num.num + val positive : Micromega.positive -> int + val n : Micromega.n -> int + val nat : Micromega.nat -> int + val index : Micromega.positive -> int + +end + +val rats_to_ints : Num.num list -> Big_int.big_int list + +val all_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list +val all_sym_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list +val try_any : (('a -> 'b option) * 'c) list -> 'a -> 'b option +val is_sublist : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool + +val gcd_list : Num.num list -> Big_int.big_int + +val extract : ('a -> 'b option) -> 'a list -> ('b * 'a) option * 'a list + +val command : string -> string array -> 'a -> 'b |