• Tej Chajed's avatar
    Support destructing exists with intro patterns · 6d1a88a5
    Tej Chajed authored and Ralf Jung's avatar Ralf Jung committed
    The syntax re-uses the existing support for pure names, namely the % and
    %H patterns. Using "[% H]" is like `iDestruct ... as (?) "H"` and using
    "[%x H]" (with the string-ident plugin) is like `iDestruct ... as (x)
    This changes how these patterns are parsed. Previously, both would have
    been handled as conjunctions (using IntoAnd or IntoSep, depending on
    whether the hypothesis is persistent or not). This means it was possible
    for the user to use "[% H]" to destruct a pure hypothesis ⌜φ ∧ ψ⌝ and
    put only the first conjunct in the Gallina context, leaving the other
    one in the IPM; such patterns will now break, since iExistDestruct
    does not handle this use case.