proofmode/spec_patterns.v · e965b669432646c5cde0b0df3b2f80af5eecf0c0 · Rice Wine / Iris

Forked from Iris / Iris

Source project has a limited visibility.

8 years ago

Merge iAssert and iPvsAssert. · e965b669

To do so, we have introduced the specialization patterns:

  =>[H1 .. Hn] and =>[-H1 .. Hn]

That generate a goal in which the view shift is preserved. These specialization
patterns can also be used for e.g. iApply.

Note that this machinery is not tied to primitive view shifts, and works for
various kinds of goal (as captured by the ToAssert type class, which describes
how to transform the asserted goal based on the main goal).

TODO: change the name of these specialization patterns to reflect this
generality.

e965b669

History

Merge iAssert and iPvsAssert.

Robbert Krebbers authored 8 years ago

To do so, we have introduced the specialization patterns:

  =>[H1 .. Hn] and =>[-H1 .. Hn]

That generate a goal in which the view shift is preserved. These specialization
patterns can also be used for e.g. iApply.

Note that this machinery is not tied to primitive view shifts, and works for
various kinds of goal (as captured by the ToAssert type class, which describes
how to transform the asserted goal based on the main goal).

TODO: change the name of these specialization patterns to reflect this
generality.