blob: db0e54efbe8835abf97e13a819cb53b547aa9806 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
datatype List = Nil | Cons(int, List)
method R(xs: List)
{
match xs
case Nil() => // currently produces a parsing error, but shouldn't
case Cons(x, Nil()) => // currently allowed
case Cons(x, Cons(y, tail)) =>
}
function F(xs: List) : int
{
match xs
case Nil() => 0 // currently produces a parsing error, but shouldn't
case Cons(x, Nil()) => 1 // currently allowed
case Cons(x, Cons(y, tail)) => 2
}
|