Wp.FilteringSequent 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 ==> pp ==> filter ~polarity:false f pSee theory/filtering.why for proofs.
val filter :
polarity:bool ->
(Lang.F.pred -> bool) ->
Lang.F.pred ->
Lang.F.predval compute : ?anti:bool -> Conditions.sequent -> Conditions.sequent