blob: bc7ff321c7399b8f6500ba2b649fe714e204a570 (
plain)
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)
}
|