X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Ftactics%2Ffourier.mli;fp=components%2Ftactics%2Ffourier.mli;h=8b26bc21abf4edd001d6d94022cd83118adf1863;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/components/tactics/fourier.mli b/components/tactics/fourier.mli
new file mode 100644
index 000000000..8b26bc21a
--- /dev/null
+++ b/components/tactics/fourier.mli
@@ -0,0 +1,27 @@
+type rational = { num : int; den : int; } 
+val print_rational : rational -> unit
+val pgcd : int -> int -> int
+val r0 : rational
+val r1 : rational
+val rnorm : rational -> rational
+val rop : rational -> rational
+val rplus : rational -> rational -> rational
+val rminus : rational -> rational -> rational
+val rmult : rational -> rational -> rational
+val rinv : rational -> rational
+val rdiv : rational -> rational -> rational
+val rinf : rational -> rational -> bool
+val rinfeq : rational -> rational -> bool
+type ineq = { coef : rational list; hist : rational list; strict : bool; } 
+val pop : 'a -> 'a list ref -> unit
+val partitionne : ineq list -> ineq list list
+val add_hist : (rational list * bool) list -> ineq list
+val ie_add : ineq -> ineq -> ineq
+val ie_emult : rational -> ineq -> ineq
+val ie_tl : ineq -> ineq
+val hd_coef : ineq -> rational
+val deduce_add : ineq list -> ineq list -> ineq list
+val deduce1 : ineq list -> int -> ineq list
+val deduce : (rational list * bool) list -> ineq list
+val unsolvable :
+  (rational list * bool) list -> (rational * bool * rational list) list