• Robbert Krebbers's avatar
    Merge iAssert and iPvsAssert. · e965b669
    Robbert Krebbers authored
    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
Name
Last commit
Last update
algebra Loading commit data...
benchmark Loading commit data...
docs Loading commit data...
heap_lang Loading commit data...
prelude Loading commit data...
program_logic Loading commit data...
proofmode Loading commit data...
tests Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
LICENSE Loading commit data...
Makefile Loading commit data...
ProofMode.md Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
naming.txt Loading commit data...