recursion - 使用序列违反了 dafny 断言

Question

这是dafny代码，第二个断言永远不会通过，任何人都可以帮助我吗？在此处输入链接描述

Answer 1

如果只使用 s[1..] 而不是等效的 s[1..|s|]，Dafny 似乎会更轻松一些。更新版本位于http://rise4fun.com/Dafny/1AQN。