CompletedNatWitness.mli 837 Bytes
 POTTIER Francois committed Jul 02, 2015 1 ``````(* This is an enriched version of [CompletedNat], where we compute not just `````` POTTIER Francois committed Jul 03, 2015 2 `````` numbers, but also sequences of matching length. *) `````` POTTIER Francois committed Jul 02, 2015 3 4 `````` (* A property is either [Finite (n, xs)], where [n] is a natural number and `````` POTTIER Francois committed Jul 03, 2015 5 `````` [xs] is a sequence of length [n]; or [Infinity]. *) `````` POTTIER Francois committed Jul 02, 2015 6 7 `````` type 'a t = `````` POTTIER Francois committed Jul 03, 2015 8 ``````| Finite of int * 'a Seq.seq `````` POTTIER Francois committed Jul 02, 2015 9 10 11 12 13 14 ``````| Infinity val bottom: 'a t val equal: 'a t -> 'b t -> bool val is_maximal: 'a t -> bool `````` POTTIER Francois committed Jul 07, 2015 15 16 ``````val compare: 'a t -> 'b t -> int `````` POTTIER Francois committed Jul 02, 2015 17 18 19 ``````val epsilon: 'a t val singleton: 'a -> 'a t `````` POTTIER Francois committed Jul 02, 2015 20 21 22 ``````val min: 'a t -> 'a t -> 'a t val add: 'a t -> 'a t -> 'a t `````` POTTIER Francois committed Jul 03, 2015 23 24 ``````val min_lazy: 'a t -> (unit -> 'a t) -> 'a t val add_lazy: 'a t -> (unit -> 'a t) -> 'a t `````` POTTIER Francois committed Jul 02, 2015 25 `````` `````` POTTIER Francois committed Jul 03, 2015 26 ``````val min_cutoff: 'a t -> (int -> 'a t) -> 'a t `````` POTTIER Francois committed Jul 03, 2015 27 ``````val add_cutoff: (* cutoff: *) int -> 'a t -> (int -> 'a t) -> 'a t `````` POTTIER Francois committed Jul 03, 2015 28 `````` `````` POTTIER Francois committed Jul 02, 2015 29 ``````val print: ('a -> string) -> 'a t -> string `````` POTTIER Francois committed Jul 03, 2015 30 ``````val to_int: 'a t -> int `````` POTTIER Francois committed Jul 07, 2015 31 ``val extract: 'a t -> 'a list``