search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.92k stars 262 forks source link

`in` operator in `requires` clause of lambda expression requires compilable equality #2184

Open cpitclaudel opened 2 years ago

cpitclaudel commented 2 years ago

Dafny accepts this:

predicate P<T>(t: T, ts: seq<T>)
  requires t in ts

… but not this:

method M<T>(ts: seq<T>) {
  var f := t requires t in ts => false; // Error: in can only be applied to expressions of sequence types that support equality (got seq<T>)
}

Is there a reason for this inconsistency?

cpitclaudel commented 2 years ago

Looks like a plain bug, since this is accepted instead:

method M<T>(ts: seq<T>) {
  ghost var pre := t => t in ts;
  var f := t requires pre(t) => false;
}