GitLab

• wp_apply could be able to apply a total WP when the goal is a partial WP, removing some duplication in heap_lang/lib.
• wp_apply could 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 \later in 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 True preconditions when the list is empty.
• When proving a triple, the postcondition could be wrapped in a fancy update, removing the need to rewrite -wp_fupd in some of our proofs. Of course, when applying a triple, that update must not be in the way.

Blocked by #130