Test/dafny4/Bug111.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

// RUN: %dafny /compile:0  "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

datatype A = A(i:int)
datatype B = B1(a1:A) | B2(a2:A)

function f(b:B):int
{
  match b
  {
    case B1(A(i)) => i
    case B2(A(j)) => j
  }
}