1

很清楚输入是一个数组，但是为什么当它执行 flag[1..] 时，它说 flag 是一个序列？这是链接： http ://rise4fun.com/Dafny/fUgu

4

1 回答 1

1

对于数组A和整数loand hi，表达式返回从index 开始的元素A[lo..hi]序列（不是数组）。对于您的程序，我建议您让所有函数在序列上运行，或者（可能对您的程序更好）向所有函数添加和参数以描绘您感​​兴趣的数组部分。hi-loAlolohi

于 2017-05-22T15:04:16.900 回答