Skip to content

Typeclass to overload WP notation.

Robbert Krebbers requested to merge ci/robbert/overloaded_wp into gen_proofmode

This MR introduces type classes Wp and Twp to overload the notations for (total) weakest preconditions.

Note that I did not try to factor out any theory about weakest preconditions. All the common theory is very much dependent on the update modality, and if we wish to use this for logics beyond Iris, we don't want it to depend on that.

@jtassaro Is this helpful for Fairis?
@jjourdan @janno Is this helpful for iGPS?

Edited by Robbert Krebbers

Merge request reports