Skip to content

Draft: Make sure -#H pattern uses intuitionistic trick

Tej Chajed requested to merge tchajed/iris-coq:fix-intuitionistic-spatial into master

This makes iDestruct (foo with "H") as "-#H2" attempt to keep H by showing the conclusion of foo is persistent.

There are a couple problems with this:

  • iDestruct "H" as "-#H" works even if H isn't persistent. This is inconsistent with the above. We could make it consistent with some more implementation.
  • (really minor incompatibility) you can no longer do iDestruct (foo with "H") as "-#H2" if the conclusion isn't persistent. Why you would have ever done this is beyond me.

Merge request reports