blob: 1992d666d24b88e7e70c44d48212ea21c2bb7728 (
plain)
1
2
3
4
5
6
7
8
9
|
// RUN: %dafny /compile:0 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function {:opaque} RefineSeqToSeq<T,U>(s:seq<T>, refine_func:T->U) : seq<U>
reads refine_func.reads;
{
if |s| == 0 then []
else RefineSeqToSeq(s[1..], refine_func)
}
|
