From 7b36d0e4c312b99b081f05b6575071b56bf12a55 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 15 Feb 2017 21:03:27 +0100
Subject: [PATCH] Add an eauto test.
---
theories/tests/proofmode.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 2c2581979..7c058426c 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -138,3 +138,7 @@ Proof.
iIntros "H". iExists _, [#10].
iSpecialize ("H" $! _ [#10]). done.
Qed.
+
+Lemma demo_16 (M : ucmraT) (P Q R : uPred M) `{!PersistentP R} :
+ P -∗ Q -∗ R -∗ R ∗ Q ∗ P ∗ R ∨ False.
+Proof. eauto with iFrame. Qed.
--
GitLab