CODEWITHSUNDEEP
arrayssequencemismatchdafny
Lilac Liu
Lilac Liu

Reputation: 49

Dafny: Why I input an array Dafny says it is a sequence

It is really clear that the input is an array, but why when it proceeds flag[1..],it says flag is a sequence? Here is the link: http://rise4fun.com/Dafny/fUgu

Upvotes: 1

Views: 991

Answers (1)

Rustan Leino
Rustan Leino

Reputation: 2087

For an array A and integers lo and hi, the expression A[lo..hi] returns the sequence (not array) of hi-lo elements from A starting at index lo. For your program, I would recommend either making all your functions operate on sequences or (probably better for your program) adding lo and hi parameters to all the functions to delineate the part of the array that you are interested in.

Upvotes: 1

Related Questions