From c28ad1d1565e60dfd14164366552efb18876872f Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Tue, 12 Aug 2014 15:31:45 -0700 Subject: Rewrote two tests to make triggering better (while waiting for better automatic triggering support in either Dafny or Boogie) --- Test/dafny3/SimpleCoinduction.dfy | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'Test/dafny3') diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy index 5be5c569..00e598c3 100644 --- a/Test/dafny3/SimpleCoinduction.dfy +++ b/Test/dafny3/SimpleCoinduction.dfy @@ -35,13 +35,13 @@ colemma {:induction false} CoUpLemma(n: int) CoUpLemma(n+1); } -lemma UpLemma_Auto(k: nat, n: int) - ensures Inc(Up(n)) ==#[k] Up(n+1); +lemma UpLemma_Auto(k: nat, n: int, nn: int) + ensures nn == n+1 ==> Inc(Up(n)) ==#[k] Up(nn); // note: it would be nice to do an automatic rewrite (from "ensures Inc(Up(n)) ==#[k] Up(n+1)") to obtain the good trigger here { } -colemma CoUpLemma_Auto(n: int) - ensures Inc(Up(n)) == Up(n+1); +colemma CoUpLemma_Auto(n: int, nn: int) + ensures nn == n+1 ==> Inc(Up(n)) == Up(nn); // see comment above { } -- cgit v1.2.3