From f28fa68497352ffb57ab2846da4cc1c1aeaf1968 Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Wed, 12 Aug 2015 22:44:50 -0700
Subject: Change the induction heuristic for lemmas to also look in
 precondition for clues about which parameters to include. As a result,
 improved many test cases (see, e.g., dafny4/NipkowKlein-chapter7.dfy!) and
 beautified some others.

---
 Test/dafny4/ACL2-extractor.dfy | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'Test/dafny4/ACL2-extractor.dfy')

diff --git a/Test/dafny4/ACL2-extractor.dfy b/Test/dafny4/ACL2-extractor.dfy
index 8fe98531..bd2c9d83 100644
--- a/Test/dafny4/ACL2-extractor.dfy
+++ b/Test/dafny4/ACL2-extractor.dfy
@@ -116,9 +116,9 @@ lemma RevLength(xs: List)
 // you can prove two lists equal by proving their elements equal
 
 lemma EqualElementsMakeEqualLists(xs: List, ys: List)
-  requires length(xs) == length(ys);
-  requires forall i :: 0 <= i < length(xs) ==> nth(i, xs) == nth(i, ys);
-  ensures xs == ys;
+  requires length(xs) == length(ys)
+  requires forall i :: 0 <= i < length(xs) ==> nth(i, xs) == nth(i, ys)
+  ensures xs == ys
 {
   match xs {
     case Nil =>
@@ -132,7 +132,7 @@ lemma EqualElementsMakeEqualLists(xs: List, ys: List)
           nth(i+1, xs) == nth(i+1, ys);
         }
       }
-      EqualElementsMakeEqualLists(xs.tail, ys.tail);
+      // EqualElementsMakeEqualLists(xs.tail, ys.tail);
   }
 }
 
-- 
cgit v1.2.3