Module Qed.BvarsSource

Bound Variables Footprints.

All provided operation are constant-time bitwise and integer operations.

Sourcetype t

An over-approximation of set of integers

Sourceval empty : t
Sourceval singleton : int -> t
Sourceval order : t -> int

Max stack of binders

Sourceval bind : t -> t

Decrease all elements in s after removing 0

Sourceval union : t -> t -> t
Sourceval closed : t -> bool

All variables are bound

Sourceval closed_at : int -> t -> bool

closed_at n a Does not contains variables k<n

Sourceval is_empty : t -> bool

No bound variables

Sourceval contains : int -> t -> bool

if contains k s returns false then k does not belong to s

Sourceval 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.

Sourceval pretty : Format.formatter -> t -> unit