• Robbert Krebbers's avatar
    Make `iDestruct ... as (cpat) "..."` work on '⌜φ⌝ ∧ P` and `⌜φ⌝ ∗ P`. · c5045145
    Robbert Krebbers authored
    The advantage is that we can directly use a Coq introduction pattern
    `cpat` to perform actions to the pure assertion. Before, this had
    to be done in several steps:
    
      iDestruct ... as "[Htmp ...]"; iDestruct "Htmp" as %cpat.
    
    That is, one had to introduce a temporary name.
    
    I expect this to be quite useful in various developments as many of
    e.g. our invariants are written as:
    
      ∃ x1 .. x2, ⌜ pure stuff ⌝ ∗ spacial stuff.
    c5045145
ticket_lock.v 6.79 KB