Test/dafny4/Bug82.dfy


1
2
3
4
5
6
7
8
9
10
11

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

function {:opaque} Reverse(id:int) : int

function RefineToMap(ReverseKey:int->int) : bool

function RefineToMapOfSeqNums() : bool
{
    RefineToMap(Reverse)
}