Module Vset

module Vset: sig .. end
Logical Sets

type set = vset list 
type vset = 
| Set of Lang.F.tau * Lang.F.term
| Singleton of Lang.F.term
| Range of Lang.F.term option * Lang.F.term option
| Descr of Lang.F.var list * Lang.F.term * Lang.F.pred
val occurs_opt : Lang.F.var -> Lang.F.term option -> bool
val occurs_vset : Lang.F.var -> vset -> bool
val occurs : Lang.F.var -> vset list -> bool
val vars_opt : Lang.F.term option -> Lang.F.Vars.t
val vars_vset : vset -> Lang.F.Vars.t
val vars : vset list -> Lang.F.Vars.t
val library : string
val adt_set : Lang.adt
val tau_of_set : ('a, Lang.adt) Qed.Logic.datatype -> ('a, Lang.adt) Qed.Logic.datatype
val p_member : Lang.lfun
val f_empty : Lang.lfun
val f_union : Lang.lfun
val f_inter : Lang.lfun
val f_range : Lang.lfun
val f_range_sup : Lang.lfun
val f_range_inf : Lang.lfun
val f_range_all : Lang.lfun
val f_singleton : Lang.lfun
val single : Lang.F.t option -> Lang.F.t option -> Lang.F.t option
val test_range : Lang.F.term ->
Lang.F.term -> Lang.F.term option -> Lang.F.term option -> Lang.F.pred
val sub_range : Lang.F.term ->
Lang.F.term -> Lang.F.t option -> Lang.F.t option -> Lang.F.pred
val in_size : Lang.F.term -> int -> Lang.F.pred
val in_range : Lang.F.term -> Lang.F.t option -> Lang.F.t option -> Lang.F.pred
val ordered : limit:bool ->
strict:bool -> Lang.F.term option -> Lang.F.term option -> Lang.F.pred
- limit: result when either parameter is None
val member : Lang.F.term -> vset list -> Lang.F.pred
val empty : 'a list
val singleton : Lang.F.term -> vset list
val range : Lang.F.term option -> Lang.F.term option -> vset list
val union : 'a list -> 'a list -> 'a list
val descr : vset -> Lang.F.var list * Lang.F.term * Lang.F.pred
val concretize_vset : vset -> Lang.F.term
val concretize : vset list -> Lang.F.term
val inter : Lang.F.term -> Lang.F.term -> Lang.F.term
val subrange : Lang.F.t option -> Lang.F.t option -> vset list -> Lang.F.pred
val subset : vset list -> vset list -> Lang.F.pred
val equal : vset list -> vset list -> Lang.F.pred
val empty_range : Lang.F.term option -> Lang.F.term option -> Lang.F.pred
val disjoint_bounds : Lang.F.term option -> Lang.F.term option -> Lang.F.pred
val disjoint_vset : vset -> vset -> Lang.F.pred
val disjoint : vset list -> vset list -> Lang.F.pred
val cartesian : ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
val map_vset : (Lang.F.term -> Lang.F.term) -> vset -> vset
val map : (Lang.F.term -> Lang.F.term) -> vset list -> vset list
val map_opt : ('a -> 'b) -> 'a option -> 'b option
val map_opp : vset list -> vset list
val lift_vset : (Lang.F.term -> Lang.F.term -> Lang.F.term) ->
vset -> vset -> vset
val lift : (Lang.F.term -> Lang.F.term -> Lang.F.term) ->
vset list -> vset list -> vset list
val pp_bound : Format.formatter -> Lang.F.term option -> unit
val bound_shift : Lang.F.term option -> Lang.F.term -> Lang.F.term option
val bound_add : Lang.F.term option -> Lang.F.term option -> Lang.F.term option
val bound_sub : Lang.F.term option -> Lang.F.term option -> Lang.F.term option
val lift_add : vset list -> vset list -> vset list
val lift_sub : vset list -> vset list -> vset list