[foooobar]

I don't think anyone is trying to sell Lean as a constructive system. The current developers certainly don't think of it that way, further evidenced by the fact that the typical way of doing computation in Lean does not involve definitional reduction, but using `#eval` with additional low level code for performance. Proof irrelevance (and quotients) were adopted with that in mind.