我是 dafny 的新手,我在获取整数的指数时遇到了麻烦
不变量 x >= 0 && y >= 0 && ((x + y) * (2^(u-1)) + 结果 == i1 + i2);
对于说“2^(u-1)”的部分,我一直收到错误提示,它期望使用位向量,但却得到了 int。我该如何解决?我需要结果是一个 int