Pure functions currently require all ensures clauses to be of the form result==.... However, for the purposes of soundness, it is sufficient for at least one of the clauses to be of this form, as long as the function has a body. This would allow pure functions to be used for writing lemmas (the function returns true and has an extra postcondition giving the relevant result). (Purity is important for lemmas because they don't create extra states.)

The main advantage of this over the more general specification forms for pure functions is that it's much easier to implement.