add characters to lean core?

Stream: general

[Eric Rodriguez]

it'd be pretty cool if we could have the characters ₌₊₋⁼⁺⁻ in Lean core (for example, hi⁺ could mean 0 < i). Where in the source are the acceptable characters controlled? And would adding these to lean3 pose any lean4 problems?

[Floris van Doorn]

You're asking that these should be valid characters in identifiers?
Counterargument: I might want ⁺ to be a postfix operation.

[Eric Rodriguez]

That makes sense, too; and I'm guessing there's no way for both to be possible