Consider intro pattern `IRewrite` (->/<-) to be intuitionistic (!856) · Merge requests · Iris / Iris

Robbert Krebbers requested to merge robbert/rewrite_pure_intro_pat into master Oct 20, 2022

This fixes a problem reported by @lelbehei at Mattermost: The introduction patterns ->/<- are not considered to be intuitionistic, hence when performing iDestruct (lem with "HP") as "->" the hypothesis HP gets needlessly consumed.

Consider intro pattern `IRewrite` (->/<-) to be intuitionistic

Merge request reports