Module Filtering

module Filtering: sig .. end

Sequent Cleaning

Erase parts of a predicate that do not satisfies the condition. The erased parts are replaced by:

Hence, we have:

See theory/filtering.why for proofs.

val filter : polarity:bool -> (Lang.F.pred -> bool) -> Lang.F.pred -> Lang.F.pred

val compute : ?anti:bool -> Conditions.sequent -> Conditions.sequent