package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

rocq-prover.org Readme Edit opam file Versions (1)

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/rocq-runtime.engine/Evd/Filter/index.html

Module `Evd.Filter`Source

Sourcetype t

Evar filters, seen as bitmasks.

Sourceval equal : t -> t -> bool

Equality over filters

Sourceval identity : t

The identity filter.

Sourceval filter_list : t -> 'a list -> 'a list

Filter a list. Sizes must coincide.

Sourceval filter_array : t -> 'a array -> 'a array

Filter an array. Sizes must coincide.

Sourceval filter_slist : t -> 'a SList.t -> 'a SList.t

Filter a sparse list. Sizes must coincide.

Sourceval extend : int -> t -> t

extend n f extends f on the left with n-th times true.

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

Sourceval 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

Sourceval restrict_upon : t -> int -> (int -> bool) -> t option

Ad-hoc primitive.

Sourceval map_along : (bool -> 'a -> bool) -> t -> 'a list -> t

Apply the function on the filter and the list. Sizes must coincide.

Sourceval make : bool list -> t

Create out of a list

Sourceval repr : t -> bool list option

Observe as a bool list.