Typeclass to overload WP notation.
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