module Filtering: sig
.. end
Sequent Cleaning
Erase parts of a predicate that do not satisfies the condition.
The erased parts are replaced by:
true
when ~polarity:false
(for hypotheses)
false
when ~polarity:true
(for goals)
Hence, we have:
filter ~polarity:true f p ==> p
p ==> filter ~polarity:false f p
See theory/filtering.why
for proofs.
val filter : polarity:bool -> (Wp.Lang.F.pred -> bool) -> Wp.Lang.F.pred -> Wp.Lang.F.pred
val compute : ?anti:bool -> Wp.Conditions.sequent -> Wp.Conditions.sequent