Allow use of #pre and #post in more tactics.

[chdoc]

It would be nice if one could use the metavariables #pre and #post in more tactics (e.g. call). In particular, it would be nice to write:

transitivity{1} (P ==> Q) (#pre ==> #post)
transitivity{2} (#pre ==> #post) (P ==> Q)

see: this Zulip topic

[fdupress]

There was also a discussion about using them in call on slack, before it went poof. (It's a bit more complex there, because the #pre and #post generally refer to local variables of the procedure being dealt with, whereas the context for the call would not.)

More generally, it would be nice to be able to use #pre<n> and #post<n> everywhere, checking that the program variables they refer to are the same in the new scope. (So that even the (P ==> Q) side in the above examples could be constructed from one-sided bits of the original contract, along with a bunch of equalities, for example.)

[chdoc]

@fdupress What's the intended meaning of #pre<n>?

[fdupress]

"The nth conjunct of #pre."

The actual syntax is #[n]pre, sorry.

[chdoc]

Do we also have #[n-m]pre to get a range of conjuncts? If not, would it be a good idea to add this?

[fdupress]

The syntax seems to be #[n:m]pre (looked in the parser), but it looks like the m is off by one (except for the bounds check, so you can never select the last conjunct in a range query).

If you open a ticket for this, I'll try to fix it this evening.

[chdoc]

If you open a ticket for this, I'll try to fix it this evening.

Your observation seems correct, issue opened as: #109