CODEWITHSUNDEEP
dafny
JRR
JRR

Reputation: 6152

How do I represent a pair (two tuple) in Dafny?

How can I write a dafny function that takes in a sequence of ints and return a sequence of Pairs? e.g., input = [1,2], output = [Pair(1,1), Pair(1,2)]

I started with 

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

which doesn't seem to work.

Upvotes: 1

Views: 913

Answers (1)

lexicalscope
lexicalscope

Reputation: 7328

You can't use new in a function, because functions are pure in Dafny they must not modify the heap. Either use 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..]) 
}

Or use tuples

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

Upvotes: 1

Related Questions