blob: bd4ded7330fafe47bfbfac55d1109d47efc75a3c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
datatype List = Nil | Cons(int, List)
method R(xs: List)
{
var a: int;
var b: int;
match xs
case Nil =>
case Cons(a, Nil()) => // this 'a' is allowed
case Cons(x, Cons(b, tail)) => // this 'b' (which is in a nested position) generates an error
}
function F(xs: List): int
{
var a := 4;
var b := 7;
match xs
case Nil => 0
case Cons(a, Nil()) => 1
case Cons(x, Cons(b, tail)) => 2
}
|
