Why aren't they usable in calc blocks anymore? If we used abbreviation instead of notation, would that be good enough?

I would also very much like to keep them available in calc-blocks.
On the up side, does this mean that the >-linter can now be removed? Because simp will see through the notation, right?

Why aren't they usable in calc blocks anymore?

The immediate reason is because the calc parser joins the proofs in the calc proof using transitivity steps. So consider the following example:

calc a = b    : p1
   ... > c    : p2

Here calc needs to combine a = b and dummy > c via transitivity. However, the second expression is actually c < dummy and Lean doesn't know how to apply transitivity here. (The calc parser also gets confused since dummy is now the second argument.)

If we used abbreviation instead of notation, would that be good enough?

The definitions ge and gt are already reducible. AFAICT the only difference between abbreviation and @[reducible, inline] def is that that the unifier unfolds the abbreviation a bit more eagerly.

I'm not sure what goes wrong exactly, but I think it boils down to the fact that e.get_app_fn.const_name returns different names for a < b and a > b. Turning ge and gt into an abbreviation doesn't change that.

@digama0 @fpvandoorn IIRC you've been heavily involved in the war against >. Do you have a small MWE of what goes wrong with >?

On the up side, does this mean that the >-linter can now be removed? Because simp will see through the notation, right?

Yes! That's the motivation for this change.

I'm not sure what goes wrong exactly, but I think it boils down to the fact that e.get_app_fn.const_name returns different names for a < b and a > b. Turning ge and gt into an abbreviation doesn't change that.

The big issue is head matching as used by simp and others, right? There is the add_key_equivalence command that is supposed to solve this issue, but AFAICS it's never been tried in either corelib or mathlib...

The big issue is head matching as used by simp and others, right?

I assume so, but I'm not an expert on the gt-issues.

There is the add_key_equivalence command that is supposed to solve this issue.

Unfortunately, the add_key_equivalence only affects kabstract used by rw. The simplifier uses the head_index class, which literally computes const_name(get_app_fn(lhs)):

Ah, you're right.

Maybe this is for another PR, but should we do the same for ne as well?

I don't think so. ne a b is actually shorter than not (eq a b), and also there are theorems in the ne namespace like ne.symm that would be lost if it was turned into a notation. Plus ne is in simp normal form so there isn't a need to eliminate it.

If we could add the right keys in the right tables rather than removing >, I'd prefer that. And if we could have a notion of synonym that can be reused, that would be even better. I can think of the same treatment for >>= vs =<<. Maybe we need an attribute?

One mild reason for > to be a definition rather than notation is that it means the pretty-printer can reproduce what the user wrote, rather than always producing < (or worse, always producing >).