Add support doing computations over sequences

1 files changed, 23 insertions, 0 deletions

diff --git a/Test/dafny0/Computations.dfy b/Test/dafny0/Computations.dfy
index 8050aded..83b2a571 100644
--- a/Test/dafny0/Computations.dfy
+++ b/Test/dafny0/Computations.dfy
@@ -184,3 +184,26 @@ ghost method test_fib3(k: nat, m: nat)
   var y := 12;

   assert y <= k && k < y + m && m == 1 ==> fib(k)==144;

 }

+

+module NeedsAllLiteralsAxiom {

+  // The following test shows that there exist an example that

+  // benefits from the all-literals axiom.  (It's not clear how

+  // important such an example is, nor is it clear what the cost

+  // of including the all-literals axiom is.)

+

+  function trick(n: nat, m: nat): nat

+    decreases n;  // note that m is not included

+  {

+    if n < m || m==0 then n else trick(n-m, m) + m

+  }

+

+  lemma lemma_trick(n: nat, m: nat)

+    ensures trick(n, m) == n;

+  {

+  }

+

+  lemma calc_trick(n: nat, m: nat)

+    ensures trick(100, 10) == 100;

+  {

+  }

+}