Dafny. Пары с булами не равны

Question

Почему эти двое терпят неудачу в Дафни?

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);
}

https://rise4fun.com/Dafny/DtDMdm

Answer 1

Я предполагаю, что это связано с внутренним боксом логических значений для универсальных типов, которые могут содержать кортежи.В любом случае, вот простой обходной путь:

lemma test(x : (int, bool)) {
  var (i, b) := x;
  assert x == (x.0, true) || x == (x.0, false);
}

Rustan