Почему эти двое терпят неудачу в Дафни?
lemma test(x : (int, bool)) {
assert x == (x.0, true) || x == (x.0, false);
}
lemma test''(v : int, x : (int, bool))
requires x.0 == v;
{
assert x == (v, true) || x == (v, false);
}
Я предполагаю, что это связано с внутренней упаковкой логических значений для общих типов, которые могут содержать кортежи. В любом случае, вот простой обходной путь:
lemma test(x : (int, bool)) {
var (i, b) := x;
assert x == (x.0, true) || x == (x.0, false);
}
Рустан