Skip to content

Hint to introduce BI version of `↔`.

Robbert Krebbers requested to merge robbert/bi_iff_hint into master 
Lemma test_auto_iff P : ⊢ P ↔ P.
Proof. auto. (* fails, fixed by this MR *) Qed.

Lemma test_auto_wand_iff P : ⊢ P ∗-∗ P.
Proof. auto. (* already worked *) Qed.
Edited by Robbert Krebbers

Merge request reports