diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-10-17 14:40:03 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-10-17 14:40:03 -0700 |
| commit | e9bee3feed78b1bb2c8e455e02eb40dc1c826eed (patch) | |
| tree | e509b8a8b72aada69e7b8074f7c8e10efb74bce3 /Test/dafny0/Datatypes.dfy | |
| parent | 6b2c5f3b96c5e0c97a42cfcc09807e9fe10c7231 (diff) | |
Added a test case for "all cases of a datatype"
Diffstat (limited to 'Test/dafny0/Datatypes.dfy')
| -rw-r--r-- | Test/dafny0/Datatypes.dfy | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy index 70177ef4..04f2a461 100644 --- a/Test/dafny0/Datatypes.dfy +++ b/Test/dafny0/Datatypes.dfy @@ -247,3 +247,8 @@ function FwdBugFunction(f: Fwd): bool }
datatype Fwd = FwdNil | FwdCons(int, Fwd);
+
+method TestAllCases(f: Fwd)
+{
+ assert f.FwdNil? || f.FwdCons?;
+}
|