Skip to content
Snippets Groups Projects

Hint to introduce BI version of `:left_right_arrow:`.

Merged Hint to introduce BI version of `:left_right_arrow:`.
robbert/bi_iff_hint into master
Merged 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

Merge request pipeline #83287 passed

Stage: build

    Merge request pipeline passed for 518bd3c4

    Approval is optional

    Merged by Ralf JungRalf Jung 1 year ago (May 30, 2023 6:05am UTC)

    Merge details

    • Changes merged into master with ab3024b1.
    • Deleted the source branch.

    Pipeline #83301 failed

    Stage: build

      Pipeline failed for ab3024b1 on master

      Activity

      Filter activity
      • Approvals
      • Assignees & reviewers
      • Comments (from bots)
      • Comments (from users)
      • Commits & branches
      • Edits
      • Labels
      • Lock status
      • Mentions
      • Merge request status
      • Tracking
      Please register or sign in to reply