On Thursday, 7 August 2014 at 18:02:08 UTC, Ola Fosheim Grøstad
wrote:
I don't see how this will work out. If it is truly unreachable
then you don't need any assume
I just gave you a concrete example of where assume(false) might
be useful for optimizing a switch statement. Just because it is
truly unreachable doesn't mean the compiler is aware of that.
It doesn't make any sense to me since I don't see how you would
discriminate between your Ps.
{P1}
while(true) skip; endwhile
{P2}
How do you define P1 and P2 to be different?
I'm not sure how you'd define them to be the same. They're
different lines of code, for one thing.
