diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-06-22 20:56:23 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-06-22 20:56:23 -0700 |
| commit | 5d7c99ee7733108b73d3f26cacc2f7480baea22a (patch) | |
| tree | dd2f726058cfc71630f3019c48b8630a24da5368 /Test/dafny0/Termination.dfy | |
| parent | da2009988989d01acb0fc523fb533853f05f193c (diff) | |
Dafny: now, equality-support determination and checking feels ripe; so, codatatypes would then be sound
Dafny: added special case to allow equality comparison against parameter-less datatype values
Diffstat (limited to 'Test/dafny0/Termination.dfy')
| -rw-r--r-- | Test/dafny0/Termination.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy index 1482dc24..bf3702ae 100644 --- a/Test/dafny0/Termination.dfy +++ b/Test/dafny0/Termination.dfy @@ -92,8 +92,8 @@ class Termination { ensures a == List.Cons(val, b);
{
match a {
- case Cons(v, r) => val := v; b := r;
- }
+ case Cons(v, r) => val := v; b := r;
+ }
}
}
|