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: Hence, we have: 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