JRR
我该如何写一个function带整数序列并返回成对序列的dafny ？例如，输入= [1,2]，输出= [对（1,1），对（1,2）]
我开始
function foo (l : seq<int>) : seq<Pair>
{
if |l| == 0 then []
else new Pair() ....
}
这似乎不起作用。
词汇镜
您不能new在函数中使用，因为函数在Dafny中是纯函数，因此它们不能修改堆。要么使用归纳数据类型
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..])
}
或使用元组
function foo (l : seq<int>) : seq<(int,int)>
{
if |l| <= 1 then []
else [(l[0],l[1])] + foo(l[2..])
}
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
编辑于
我来说两句