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].

7 files changed, 214 insertions, 65 deletions

diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index c94c697d..45d8a2c9 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -715,7 +715,7 @@ namespace Microsoft.Dafny
   {

     protected readonly Expression k;

     protected readonly ErrorReporter reporter;

-    readonly string suffix;

+    protected readonly string suffix;

     protected FixpointCloner(Expression k, ErrorReporter reporter)

     {

       Contract.Requires(k != null);

@@ -724,6 +724,18 @@ namespace Microsoft.Dafny
       this.reporter = reporter;

       this.suffix = string.Format("#[{0}]", Printer.ExprToString(k));

     }

+    protected Expression CloneCallAndAddK(FunctionCallExpr e) {

+      Contract.Requires(e != null);

+      var receiver = CloneExpr(e.Receiver);

+      var args = new List<Expression>();

+      args.Add(k);

+      foreach (var arg in e.Args) {

+        args.Add(CloneExpr(arg));

+      }

+      var fexp = new FunctionCallExpr(Tok(e.tok), e.Name + "#", receiver, e.OpenParen, args);

+      reporter.Info(MessageSource.Cloner, e.tok, e.Name + suffix);

+      return fexp;

+    }

   }

 

   /// <summary>

@@ -733,6 +745,7 @@ namespace Microsoft.Dafny
   /// precondition (resp. postcondition) of the inductive lemma's (resp. colemma's) corresponding prefix lemma.

   /// It is assumed that the source expression has been resolved.  Note, the "k" given to the constructor

   /// is not cloned with each use; it is simply used as is.

+  /// The resulting expression needs to be resolved by the caller.

   /// </summary>

   class FixpointLemmaSpecificationSubstituter : FixpointCloner

   {

@@ -756,15 +769,7 @@ namespace Microsoft.Dafny
       } else if (expr is FunctionCallExpr) {

         var e = (FunctionCallExpr)expr;

         if (friendlyCalls.Contains(e)) {

-          var receiver = CloneExpr(e.Receiver);

-          var args = new List<Expression>();

-          args.Add(k);

-          foreach (var arg in e.Args) {

-            args.Add(CloneExpr(arg));

-          }

-          var fexp = new FunctionCallExpr(Tok(e.tok), e.Name + "#", receiver, e.OpenParen, args);

-          reporter.Info(MessageSource.Cloner, e.tok, e.Name);

-          return fexp;

+          return CloneCallAndAddK(e);

         }

       } else if (expr is BinaryExpr && isCoContext) {

         var e = (BinaryExpr)expr;

@@ -774,7 +779,7 @@ namespace Microsoft.Dafny
           var B = CloneExpr(e.E1);

           var teq = new TernaryExpr(Tok(e.tok), op, k, A, B);

           var opString = op == TernaryExpr.Opcode.PrefixEqOp ? "==" : "!=";

-          reporter.Info(MessageSource.Cloner, e.tok, opString);

+          reporter.Info(MessageSource.Cloner, e.tok, opString + suffix);

           return teq;

         }

       }

@@ -803,19 +808,77 @@ namespace Microsoft.Dafny
   }

 

   /// <summary>

-  /// The task of the FixpointLemmaBodyCloner is to fill in the implicit _k-1 arguments in recursive inductive/co-lemma calls.

+  /// The task of the FixpointLemmaBodyCloner is to fill in the implicit _k-1 arguments in recursive inductive/co-lemma calls

+  /// and in calls to the focal predicates.

   /// The source statement and the given "k" are assumed to have been resolved.

   /// </summary>

   class FixpointLemmaBodyCloner : FixpointCloner

   {

     readonly FixpointLemma context;

-    public FixpointLemmaBodyCloner(FixpointLemma context, Expression k, ErrorReporter reporter)

+    readonly ISet<FixpointPredicate> focalPredicates;

+    public FixpointLemmaBodyCloner(FixpointLemma context, Expression k, ISet<FixpointPredicate> focalPredicates, ErrorReporter reporter)

       : base(k, reporter)

     {

       Contract.Requires(context != null);

       Contract.Requires(k != null);

       Contract.Requires(reporter != null);

       this.context = context;

+      this.focalPredicates = focalPredicates;

+    }

+    public override Expression CloneExpr(Expression expr) {

+      if (DafnyOptions.O.RewriteFocalPredicates) {

+        if (expr is FunctionCallExpr) {

+          var e = (FunctionCallExpr)expr;

+#if DEBUG_PRINT

+          if (e.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => e.Function.Name == p.Name + "#")) {

+            Console.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(e));

+          }

+#endif

+          // Note, we don't actually ever get here, because all calls will have been parsed as ApplySuffix.

+          // However, if something changes in the future (for example, some rewrite that changing an ApplySuffix

+          // to its resolved FunctionCallExpr), then we do want this code, so with the hope of preventing

+          // some error in the future, this case is included.  (Of course, it is currently completely untested!)

+          var f = e.Function as FixpointPredicate;

+          if (f != null && focalPredicates.Contains(f)) {

+#if DEBUG_PRINT

+            var r = CloneCallAndAddK(e);

+            Console.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", e.tok.filename, e.tok.line, e.tok.col, Printer.ExprToString(r));

+            return r;

+#else

+            return CloneCallAndAddK(e);

+#endif

+          }

+        } else if (expr is ApplySuffix) {

+          var apply = (ApplySuffix)expr;

+          if (!apply.WasResolved()) {

+            // Since we're assuming the enclosing statement to have been resolved, this ApplySuffix must

+            // be part of an ExprRhs that actually designates a method call.  Such an ApplySuffix does

+            // not get listed as being resolved, but its components (like its .Lhs) are resolved.

+            var mse = (MemberSelectExpr)apply.Lhs.Resolved;

+            Contract.Assume(mse.Member is Method);

+          } else {

+            var fce = apply.Resolved as FunctionCallExpr;

+            if (fce != null) {

+#if DEBUG_PRINT

+              if (fce.Function.Name.EndsWith("#") && Contract.Exists(focalPredicates, p => fce.Function.Name == p.Name + "#")) {

+                Console.WriteLine("{0}({1},{2}): DEBUG: Possible opportunity to rely on new rewrite: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(fce));

+              }

+#endif

+              var f = fce.Function as FixpointPredicate;

+              if (f != null && focalPredicates.Contains(f)) {

+#if DEBUG_PRINT

+                var r = CloneCallAndAddK(fce);

+                Console.WriteLine("{0}({1},{2}): DEBUG: Rewrote extreme predicate into prefix predicate: {3}", fce.tok.filename, fce.tok.line, fce.tok.col, Printer.ExprToString(r));

+                return r;

+#else

+                return CloneCallAndAddK(fce);

+#endif

+              }

+            }

+          }

+        }

+      }

+      return base.CloneExpr(expr);

     }

     public override AssignmentRhs CloneRHS(AssignmentRhs rhs) {

       var r = rhs as ExprRhs;

@@ -839,7 +902,7 @@ namespace Microsoft.Dafny
           apply.Args.ForEach(arg => args.Add(CloneExpr(arg)));

           var applyClone = new ApplySuffix(Tok(apply.tok), lhsClone, args);

           var c = new ExprRhs(applyClone);

-          reporter.Info(MessageSource.Cloner, apply.Lhs.tok, mse.Member.Name);

+          reporter.Info(MessageSource.Cloner, apply.Lhs.tok, mse.Member.Name + suffix);

           return c;

         }

       }

diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs
index 59d0eb2c..2d8756d2 100644
--- a/Source/Dafny/DafnyOptions.cs
+++ b/Source/Dafny/DafnyOptions.cs
@@ -65,11 +65,12 @@ namespace Microsoft.Dafny
     public bool AllowGlobals = false;
     public bool CountVerificationErrors = true;
     public bool Optimize = false;
-    public bool AutoTriggers = false;
+    public bool AutoTriggers = false;

+    public bool RewriteFocalPredicates = false;

     public bool PrintTooltips = false;
     public bool PrintStats = false;
     public bool PrintFunctionCallGraph = false;
-    public bool WarnShadowing = false;
+    public bool WarnShadowing = false;

     public bool IronDafny = 
 #if ENABLE_IRONDAFNY 
       true
@@ -216,12 +217,20 @@ namespace Microsoft.Dafny
 
         case "printTooltips":
           PrintTooltips = true;
-          return true;
+          return true;

+

+        case "autoTriggers": {

+            int autoTriggers = 0;

+            if (ps.GetNumericArgument(ref autoTriggers, 2)) {

+              AutoTriggers = autoTriggers == 1;

+            }

+            return true;

+          }
 
-        case "autoTriggers": {
-            int autoTriggers = 0;
-            if (ps.GetNumericArgument(ref autoTriggers, 2)) {
-              AutoTriggers = autoTriggers == 1;
+        case "rewriteFocalPredicates": {

+            int rewriteFocalPredicates = 0;

+            if (ps.GetNumericArgument(ref rewriteFocalPredicates, 2)) {

+              RewriteFocalPredicates = rewriteFocalPredicates == 1;
             }
             return true;
           }
@@ -369,6 +378,10 @@ namespace Microsoft.Dafny
                 0 (default) - Do not generate {:trigger} annotations for user-level quantifiers.
                 1 - Add a {:trigger} to each user-level quantifier. Existing
                               annotations are preserved.
+  /rewriteFocalPredicates:<n>
+                0 (default) - Don't rewrite predicates in the body of prefix lemmas.
+                1 - In the body of prefix lemmas, rewrite any use of a focal predicate
+                    P to P#[_k-1].
   /optimize     Produce optimized C# code, meaning:
                   - selects optimized C# prelude by passing 
                     /define:DAFNY_USE_SYSTEM_COLLECTIONS_IMMUTABLE to csc.exe (requires 
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 36464925..7a540722 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1565,6 +1565,7 @@ namespace Microsoft.Dafny
             continue;  // something went wrong during registration of the prefix lemma (probably a duplicated fixpoint-lemma name)

           }

           var k = prefixLemma.Ins[0];

+          var focalPredicates = new HashSet<FixpointPredicate>();

           if (com is CoLemma) {

             // compute the postconditions of the prefix lemma

             Contract.Assume(prefixLemma.Ens.Count == 0);  // these are not supposed to have been filled in before

@@ -1574,6 +1575,12 @@ namespace Microsoft.Dafny
               var subst = new FixpointLemmaSpecificationSubstituter(coConclusions, new IdentifierExpr(k.tok, k.Name), this.reporter, true);

               var post = subst.CloneExpr(p.E);

               prefixLemma.Ens.Add(new MaybeFreeExpression(post, p.IsFree));

+              foreach (var e in coConclusions) {

+                var fce = e as FunctionCallExpr;

+                if (fce != null) {  // the other possibility is that "e" is a BinaryExpr

+                  focalPredicates.Add((CoPredicate)fce.Function);

+                }

+              }

             }

           } else {

             // compute the preconditions of the prefix lemma

@@ -1584,13 +1591,18 @@ namespace Microsoft.Dafny
               var subst = new FixpointLemmaSpecificationSubstituter(antecedents, new IdentifierExpr(k.tok, k.Name), this.reporter, false);

               var pre = subst.CloneExpr(p.E);

               prefixLemma.Req.Add(new MaybeFreeExpression(pre, p.IsFree));

+              foreach (var e in antecedents) {

+                var fce = (FunctionCallExpr)e;  // we expect "antecedents" to contain only FunctionCallExpr's

+                focalPredicates.Add((InductivePredicate)fce.Function);

+              }

             }

           }

+          reporter.Info(MessageSource.Resolver, com.tok, string.Format("{0} specialized for {1}", com.PrefixLemma.Name, Util.Comma(focalPredicates, p => p.Name)));

           // Compute the statement body of the prefix lemma

           Contract.Assume(prefixLemma.Body == null);  // this is not supposed to have been filled in before

           if (com.Body != null) {

             var kMinusOne = new BinaryExpr(com.tok, BinaryExpr.Opcode.Sub, new IdentifierExpr(k.tok, k.Name), new LiteralExpr(com.tok, 1));

-            var subst = new FixpointLemmaBodyCloner(com, kMinusOne, this.reporter);

+            var subst = new FixpointLemmaBodyCloner(com, kMinusOne, focalPredicates, this.reporter);

             var mainBody = subst.CloneBlockStmt(com.Body);

             var kPositive = new BinaryExpr(com.tok, BinaryExpr.Opcode.Lt, new LiteralExpr(com.tok, 0), new IdentifierExpr(k.tok, k.Name));

             var condBody = new IfStmt(com.BodyStartTok, mainBody.EndTok, kPositive, mainBody, null);

@@ -3571,7 +3583,7 @@ namespace Microsoft.Dafny
             var substituter = new Translator.AlphaConverting_Substituter(cs.Receiver, argsSubstMap, new Dictionary<TypeParameter, Type>(), new Translator(resolver.reporter));

             foreach (var ens in cs.Method.Ens) {

               var p = substituter.Substitute(ens.E);  // substitute the call's actuals for the method's formals

-              resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ensures " + Printer.ExprToString(p) + ";");

+              resolver.reporter.Info(MessageSource.Resolver, s.Tok, "ensures " + Printer.ExprToString(p));

             }

           }

         }

diff --git a/Test/dafny0/CoinductiveProofs.dfy b/Test/dafny0/CoinductiveProofs.dfy
index d990ae51..0dce8af9 100644
--- a/Test/dafny0/CoinductiveProofs.dfy
+++ b/Test/dafny0/CoinductiveProofs.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /rewriteFocalPredicates:1 "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

 codatatype Stream<T> = Cons(head: T, tail: Stream)

@@ -12,6 +12,7 @@ copredicate Pos(s: Stream<int>)
 {

   0 < s.head && Pos(s.tail)

 }

+predicate FullPos(s: Stream<int>) { Pos(s) }  // a way in the test file to sidestep focal-predicate rewrites

 

 colemma {:induction false} PosLemma0(n: int)

   requires 1 <= n;

@@ -26,7 +27,25 @@ colemma {:induction false} PosLemma1(n: int)
 {

   PosLemma1(n + 1);

   if (*) {

-    assert Pos(Upward(n + 1));  // error: cannot conclude this here, because we only have prefix predicates

+    assert FullPos(Upward(n + 1));  // error: cannot conclude this here, because we only have prefix predicates

+  }

+}

+

+colemma {:induction false} PosLemma2(n: int)

+  requires 1 <= n;

+  ensures Pos(Upward(n));

+{

+  PosLemma2(n + 1);

+  if (*) {

+    assert Pos(Upward(n + 1));  // Pos gets rewritten to Pos#[_k-1], which does hold

+  } else if (*) {

+    assert Pos#[_k-1](Upward(n + 1));  // explicitly saying Pos#[_k-1] also holds

+  } else if (*) {

+    assert Pos#[_k](Upward(n + 1));  // error: this is not known to hold for _k and n+1

+  } else if (*) {

+    assert Pos#[_k](Upward(n));  // but it does hold with Pos#[_k] and n (which is the postcondition of the prefix lemma)

+  } else if (*) {

+    assert Pos#[_k+1](Upward(n));  // error: this is too much to ask for

   }

 }

 

@@ -65,13 +84,29 @@ colemma {:induction false} AlwaysLemma_X1(s: Stream)
 {

   AlwaysLemma_X1(s);  // this is the right proof

 }

+predicate FullX(s: Stream) { X(s) }  // a way in the test file to sidestep focal-predicate rewrites

 

 colemma {:induction false} AlwaysLemma_X2(s: Stream)

   ensures X(s);

 {

   AlwaysLemma_X2(s);

   if (*) {

-    assert X(s);  // error: cannot conclude the full predicate here

+    assert FullX(s);  // error: cannot conclude the full predicate here

+  }

+}

+

+colemma {:induction false} AlwaysLemma_X3(s: Stream)

+  ensures X(s);

+{

+  AlwaysLemma_X3(s);

+  if (*) {

+    assert X(s);  // holds, because it gets rewritten to X#[_k-1]

+  } else if (*) {

+    assert X#[_k-1](s);  // explicitly saying X#[_k-1] also holds

+  } else if (*) {

+    assert X#[_k](s);  // in fact, X#[_k] holds, too (which is the postcondition of the prefix lemma)

+  } else if (*) {

+    assert X#[_k+1](s);  // as it turns out, this holds too, since the definition of X makes X#[_k+1] equal X#[_k]

   }

 }

 

@@ -79,6 +114,7 @@ copredicate Y(s: Stream)  // this is equivalent to always returning 'true'
 {

   Y(s.tail)

 }

+predicate FullY(s: Stream) { Y(s) }  // a way in the test file to sidestep focal-predicate rewrites

 

 colemma {:induction false} AlwaysLemma_Y0(s: Stream)

   ensures Y(s);  // prove that Y(s) really is always 'true'

@@ -97,7 +133,24 @@ colemma {:induction false} AlwaysLemma_Y2(s: Stream)
 {

   AlwaysLemma_Y2(s.tail);

   if (*) {

-    assert Y(s.tail);  // error: not provable here

+    assert FullY(s.tail);  // error: not provable here

+  }

+}

+

+colemma {:induction false} AlwaysLemma_Y3(s: Stream)

+  ensures Y(s);

+{

+  AlwaysLemma_Y3(s.tail);

+  if (*) {

+    assert Y(s.tail);  // this holds, because it's rewritten to Y#[_k-1]

+  } else if (*) {

+    assert Y#[_k-1](s.tail);

+  } else if (*) {

+    assert Y#[_k](s.tail);  // error: not known to hold for _k and s.tail

+  } else if (*) {

+    assert Y#[_k](s);  // this is also the postcondition of the prefix lemma

+  } else if (*) {

+    assert Y#[_k+1](s);  // error: this is too much to ask for

   }

 }

 

diff --git a/Test/dafny0/CoinductiveProofs.dfy.expect b/Test/dafny0/CoinductiveProofs.dfy.expect
index 2a5a2b0b..c4f4c405 100644
--- a/Test/dafny0/CoinductiveProofs.dfy.expect
+++ b/Test/dafny0/CoinductiveProofs.dfy.expect
@@ -1,50 +1,77 @@
-CoinductiveProofs.dfy(29,11): Error: assertion violation

+CoinductiveProofs.dfy(30,11): Error: assertion violation

+CoinductiveProofs.dfy(15,36): Related location

 CoinductiveProofs.dfy(13,16): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon6_Then

-CoinductiveProofs.dfy(59,0): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(58,10): Related location: This is the postcondition that might not hold.

-CoinductiveProofs.dfy(54,2): Related location

+CoinductiveProofs.dfy(44,11): Error: assertion violation

+CoinductiveProofs.dfy(13,16): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon13_Then

+    (0,0): anon16_Then

+CoinductiveProofs.dfy(48,11): Error: assertion violation

+CoinductiveProofs.dfy(13,16): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon13_Then

+    (0,0): anon18_Then

+CoinductiveProofs.dfy(78,0): Error BP5003: A postcondition might not hold on this return path.

+CoinductiveProofs.dfy(77,10): Related location: This is the postcondition that might not hold.

+CoinductiveProofs.dfy(73,2): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-CoinductiveProofs.dfy(74,11): Error: assertion violation

-CoinductiveProofs.dfy(54,2): Related location

+CoinductiveProofs.dfy(94,11): Error: assertion violation

+CoinductiveProofs.dfy(87,29): Related location

+CoinductiveProofs.dfy(73,2): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon6_Then

-CoinductiveProofs.dfy(91,0): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(90,10): Related location: This is the postcondition that might not hold.

-CoinductiveProofs.dfy(80,2): Related location

+CoinductiveProofs.dfy(127,0): Error BP5003: A postcondition might not hold on this return path.

+CoinductiveProofs.dfy(126,10): Related location: This is the postcondition that might not hold.

+CoinductiveProofs.dfy(115,2): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-CoinductiveProofs.dfy(100,11): Error: assertion violation

-CoinductiveProofs.dfy(80,2): Related location

+CoinductiveProofs.dfy(136,11): Error: assertion violation

+CoinductiveProofs.dfy(117,29): Related location

+CoinductiveProofs.dfy(115,2): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon6_Then

-CoinductiveProofs.dfy(111,0): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(110,10): Related location: This is the postcondition that might not hold.

-CoinductiveProofs.dfy(106,2): Related location

+CoinductiveProofs.dfy(149,11): Error: assertion violation

+CoinductiveProofs.dfy(115,2): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon13_Then

+    (0,0): anon16_Then

+CoinductiveProofs.dfy(153,11): Error: assertion violation

+CoinductiveProofs.dfy(115,2): Related location

+Execution trace:

+    (0,0): anon0

+    (0,0): anon13_Then

+    (0,0): anon18_Then

+CoinductiveProofs.dfy(164,0): Error BP5003: A postcondition might not hold on this return path.

+CoinductiveProofs.dfy(163,10): Related location: This is the postcondition that might not hold.

+CoinductiveProofs.dfy(159,2): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-CoinductiveProofs.dfy(150,0): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(149,21): Related location: This is the postcondition that might not hold.

+CoinductiveProofs.dfy(203,0): Error BP5003: A postcondition might not hold on this return path.

+CoinductiveProofs.dfy(202,21): Related location: This is the postcondition that might not hold.

 CoinductiveProofs.dfy(4,23): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

-CoinductiveProofs.dfy(156,0): Error BP5003: A postcondition might not hold on this return path.

-CoinductiveProofs.dfy(155,21): Related location: This is the postcondition that might not hold.

+CoinductiveProofs.dfy(209,0): Error BP5003: A postcondition might not hold on this return path.

+CoinductiveProofs.dfy(208,21): Related location: This is the postcondition that might not hold.

 CoinductiveProofs.dfy(4,23): Related location

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

 

-Dafny program verifier finished with 35 verified, 8 errors

+Dafny program verifier finished with 42 verified, 12 errors

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