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
strict
: if true
, comparison is <
instead of <=
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