diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-04-05 18:09:08 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-04-05 18:09:08 -0700 |
| commit | c1a561a3321335376475611d9313b3ac46478841 (patch) | |
| tree | 25105cc7aed2916ac3e4e94fc4f568104def191d /Test/dafny0/AdvancedLHS.dfy | |
| parent | df37590de103fb9c9a9d0d664611d0de05907e22 (diff) | |
Dafny: don't require parentheses in syntax of "choose" statements
Diffstat (limited to 'Test/dafny0/AdvancedLHS.dfy')
| -rw-r--r-- | Test/dafny0/AdvancedLHS.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/AdvancedLHS.dfy b/Test/dafny0/AdvancedLHS.dfy index b73af758..4f80eade 100644 --- a/Test/dafny0/AdvancedLHS.dfy +++ b/Test/dafny0/AdvancedLHS.dfy @@ -8,7 +8,7 @@ class C { x := new C;
x := new C.Init();
havoc x;
- x := choose(S);
+ x := choose S;
// test evaluation order
var c := x;
|