helm/software/components/tactics/fourier.mli

   1 type rational = { num : int; den : int; }
   2 val print_rational : rational -> unit
   3 val pgcd : int -> int -> int
   4 val r0 : rational
   5 val r1 : rational
   6 val rnorm : rational -> rational
   7 val rop : rational -> rational
   8 val rplus : rational -> rational -> rational
   9 val rminus : rational -> rational -> rational
  10 val rmult : rational -> rational -> rational
  11 val rinv : rational -> rational
  12 val rdiv : rational -> rational -> rational
  13 val rinf : rational -> rational -> bool
  14 val rinfeq : rational -> rational -> bool
  15 type ineq = { coef : rational list; hist : rational list; strict : bool; }
  16 val pop : 'a -> 'a list ref -> unit
  17 val partitionne : ineq list -> ineq list list
  18 val add_hist : (rational list * bool) list -> ineq list
  19 val ie_add : ineq -> ineq -> ineq
  20 val ie_emult : rational -> ineq -> ineq
  21 val ie_tl : ineq -> ineq
  22 val hd_coef : ineq -> rational
  23 val deduce_add : ineq list -> ineq list -> ineq list
  24 val deduce1 : ineq list -> int -> ineq list
  25 val deduce : (rational list * bool) list -> ineq list
  26 val unsolvable :
  27   (rational list * bool) list -> (rational * bool * rational list) list