pure functions cannot be removed, actually: pure vs. total

[Timon Gehr]

On 11.06.2018 16:39, Timon Gehr wrote:
> 
> FeepingCreature's example does not really qualify as a do-nothing loop, 
> because the loop produces a value that you (presumably) later access.

Hm, ok. The problem is actually there, but it is not that the 'find' 
call will get removed, it is that the loop within find's implementation 
will be seen as doing nothing and producing nothing after inlining, 
breaking find's postcondition.