Dafnyでペア（2タプル）を表すにはどうすればいいですか？

Question

どのようにして、一連のintを受け取り、一連のペアを返すダフニーfunctionを書くことができますか？例えば、入力= [1,2]、出力= [ペア（1,1）、ペア（1,2）]

私が動作していないよう

function foo (l : seq<int>) : seq<Pair> 
{ 
    if |l| == 0 then [] 
    else new Pair() .... 
} 

で開始。

Answer 1

関数内でnewを使用することはできません。関数はDafnyでは純粋なので、ヒープは変更しないでください。どちらかinductive datatypes

datatype Pair = Pair(fst:int, snd:int) 

function foo (l : seq<int>) : seq<Pair> 
{ 
    if |l| <= 1 then [] 
    else [Pair(l[0],l[1])] + foo(l[2..]) 
} 

を使用するか、使用tuples

function foo (l : seq<int>) : seq<(int,int)> 
{ 
    if |l| <= 1 then [] 
    else [(l[0],l[1])] + foo(l[2..]) 
}