diff options
| author |  Rustan Leino <unknown> | 2013-06-20 14:55:57 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-06-20 14:55:57 -0700 |
| commit | cbb62c37bcfe5fa6d3b41f30d7a2c4ee711fc036 (patch) | |
| tree | fc9804f3d8aa9eaffa226a62c006a4a7fa8d4e75 /Test/dafny0/Datatypes.dfy | |
| parent | 5d1b6d2b134d05311380abb444c04031a263b7f6 (diff) | |
Make "datatype constructor cases" axiom available whenever the discriminator for any constructor is uttered.
Diffstat (limited to 'Test/dafny0/Datatypes.dfy')
| -rw-r--r-- | Test/dafny0/Datatypes.dfy | 17 |
1 files changed, 16 insertions, 1 deletions
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy index 04f2a461..f2884b6a 100644 --- a/Test/dafny0/Datatypes.dfy +++ b/Test/dafny0/Datatypes.dfy @@ -246,9 +246,24 @@ function FwdBugFunction(f: Fwd): bool // There was once a bug in Dafny, where this had caused an ill-defined Boogie program.
}
-datatype Fwd = FwdNil | FwdCons(int, Fwd);
+datatype Fwd = FwdNil | FwdCons(int, w: Fwd);
method TestAllCases(f: Fwd)
{
assert f.FwdNil? || f.FwdCons?;
}
+
+method TestAllCases_Inside(f: Fwd)
+{
+ if f.FwdCons? {
+ assert f.w.FwdNil? || f.w.FwdCons?;
+ }
+}
+
+class ContainsFwd {
+ var fwd: Fwd;
+ method TestCases()
+ {
+ assert fwd.FwdNil? || fwd.FwdCons?;
+ }
+}
|