[bitc-dev] Syntax of FORALL
Jonathan S. Shapiro
shap at eros-os.com
Sun Oct 5 14:02:57 CDT 2008
On Sun, 2008-10-05 at 11:35 -0400, Jonathan S. Shapiro wrote:
> The other day, I unthinkingly wrote REQUIRE instead, as in:
> REQUIRE Eql('a) IN
> DEF ReallyEquals(x:'a, y) x == y;
Okay. I can see at least one reason not to do this, which is that
preconditions are not part of type in BitC. While we can write REQUIRE
here, we still need to write forall at qualified types.
That may or may not be a compelling objection, but it is at least one
reason to consider more carefully.
More information about the bitc-dev