Module Wp.Filtering

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