You can search for identifiers within the package.
in-package search v0.2.0
qed
Qed.Bvars
Bound Variables Footprints.
All provided operation are constant-time bitwise and integer operations.
type t
An over-approximation of set of integers
val empty : t
val singleton : int -> t
val order : t -> int
Max stack of binders
val bind : t -> t
Decrease all elements in s after removing 0
s
0
val union : t -> t -> t
val closed : t -> bool
All variables are bound
val closed_at : int -> t -> bool
closed_at n a Does not contains variables k<n
closed_at n a
k<n
val is_empty : t -> bool
No bound variables
val contains : int -> t -> bool
if contains k s returns false then k does not belong to s
contains k s
false
k
val overlap : int -> int -> t -> bool
if may_overlap k n s returns false then no variable i with k<=i<k+n occurs in s.
may_overlap k n s
i
k<=i<k+n
val pretty : Format.formatter -> t -> unit