[bitc-dev] Syntax of FORALL

[Jonathan S. Shapiro]

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.

shap