Closed grunweg closed 4 months ago
Per the reasoning in mathlib4#10816: these are confusing to newcomers, hence we try to avoid them.
They are still used somewhat in core, and in Mathlib/Logic/Basic - which is why I worded this relatively softly.
Per the reasoning in mathlib4#10816: these are confusing to newcomers, hence we try to avoid them.
They are still used somewhat in core, and in Mathlib/Logic/Basic - which is why I worded this relatively softly.