wp_apply/Texan triple improvements
wp_applycould be able to apply a total WP when the goal is a partial WP, removing some duplication in heap_lang/lib.
wp_applycould automatically try to prove that the expression is not a value, and then apply some variant of
wp_step. This would remove the need to have a
\laterin the definition of Texan triples, making them equivalent to a WP in all cases (as opposed to just the non-value case). I think right now I regret that we decided for Texan triples to contain the
\later, this makes them slightly harder to teach and destroys their equivalence with WP/"normal" triples.
[More far-fetched?] Make the precondition of Texan triples a list of assertions, so that we can (a) desugar them to something curried, and (b) not have silly
Truepreconditions when the list is empty.
When proving a triple, the postcondition could be wrapped in a fancy update, removing the need to
rewrite -wp_fupdin some of our proofs. Of course, when applying a triple, that update must not be in the way.
What about some support for introducing the postcondition into the context (avoiding a manual
iIntrosall the time)?
Blocked by #130