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.
