From 1885f7d7d1fb9bd6ceb8220450dbb5d890501337 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Fri, 2 Oct 2015 15:26:56 -0700
Subject: Hover text includes #[_k-1] suffix for terms rewritten in prefix
 predicates/lemmas (this fixes an item from the wishlist). Include in hover
 text the extreme predicates for which an extreme lemmas has been rewritten
 (but don't include ==# in this list--or should it perhaps be included?).
 Under a (temporary) switch /rewriteFocalPredicates, each use of a focal
 predicate P in a prefix lemma is rewritten into P#[_k-1].

---
 Test/wishlist/tooltips-on-inductive-lemmas.dfy        | 12 ------------
 Test/wishlist/tooltips-on-inductive-lemmas.dfy.expect |  7 -------
 2 files changed, 19 deletions(-)
 delete mode 100644 Test/wishlist/tooltips-on-inductive-lemmas.dfy
 delete mode 100644 Test/wishlist/tooltips-on-inductive-lemmas.dfy.expect

(limited to 'Test/wishlist')

diff --git a/Test/wishlist/tooltips-on-inductive-lemmas.dfy b/Test/wishlist/tooltips-on-inductive-lemmas.dfy
deleted file mode 100644
index 1bd25437..00000000
--- a/Test/wishlist/tooltips-on-inductive-lemmas.dfy
+++ /dev/null
@@ -1,12 +0,0 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-inductive lemma P()
-  requires Q() { // WISH the tooltip for this was broken at some point between
-                 // revisions 94ee216fe0cd (1179) and bd779dda3b3d (1785)
-  P();
-}
-
-inductive predicate Q() {
-  Q()
-}
diff --git a/Test/wishlist/tooltips-on-inductive-lemmas.dfy.expect b/Test/wishlist/tooltips-on-inductive-lemmas.dfy.expect
deleted file mode 100644
index 4d036eef..00000000
--- a/Test/wishlist/tooltips-on-inductive-lemmas.dfy.expect
+++ /dev/null
@@ -1,7 +0,0 @@
-tooltips-on-inductive-lemmas.dfy(5,11): Info: Q
-tooltips-on-inductive-lemmas.dfy(7,2): Info: P
-tooltips-on-inductive-lemmas.dfy(11,2): Info: Q#[_k - 1]
-tooltips-on-inductive-lemmas.dfy(4,16): Info: P# {:induction _k}
-tooltips-on-inductive-lemmas.dfy(4,16): Info: P# decreases _k
-
-Dafny program verifier finished with 3 verified, 0 errors
-- 
cgit v1.2.3