Module `Evd.Filter`

type t: Evar filters, seen as bitmasks.

val equal : t -> t -> bool: Equality over filters

val identity : t: The identity filter.

val filter_list : t -> 'a list -> 'a list: Filter a list. Sizes must coincide.

val filter_array : t -> 'a array -> 'a array: Filter an array. Sizes must coincide.

val extend : int -> t -> t: extend n f extends f on the left with n-th times true.

val compose : t -> t -> t: Horizontal composition : compose f1 f2 only keeps parts of f2 where f1 is set. In particular, f1 and f2 must have the same length.

val apply_subfilter : t -> bool list -> t: apply_subfilter f1 f2 applies filter f2 where f1 is true. In particular, the length of f2 is the number of times f1 is true

val restrict_upon : t -> int -> (int -> bool) -> t option: Ad-hoc primitive.

val map_along : (bool -> 'a -> bool) -> t -> 'a list -> t: Apply the function on the filter and the list. Sizes must coincide.

val make : bool list -> t: Create out of a list

val repr : t -> bool list option: Observe as a bool list.