Comment by noodlesUK

I feel like a proof assistant is amongst the worst places to have something like this rather than (I don’t know how lean works) raising an error. What are the justifications for this convention?