Closed adomasbaliuka closed 3 weeks ago
We are considering adding a linter to Mathlib (https://github.com/leanprover-community/mathlib4/pull/16215) that checks all unicode characters against a whitelist.
Since the character '﷼': Unicode U+FDFC (category Sc: Symbol, currency)
is currently not used in Mathlib and expects right-to-left text flow, we would disallow it
. (E.g., consider this code, which is currently allowed in Lean (note the meaning of "infix"):
infix:50 " ﷼ " => Add.add def x := 2 ﷼ 2
For consistency, all characters in the abbreviations JSON should be allowed by the linter.
Could we remove it from the abbreviations set here?
@PatrickMassot advocated for this at Zulip
Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.
Proposal
We are considering adding a linter to Mathlib (https://github.com/leanprover-community/mathlib4/pull/16215) that checks all unicode characters against a whitelist.
Since the character '﷼': Unicode U+FDFC (category Sc: Symbol, currency)
is currently not used in Mathlib and expects right-to-left text flow, we would disallow it
. (E.g., consider this code, which is currently allowed in Lean (note the meaning of "infix"):
For consistency, all characters in the abbreviations JSON should be allowed by the linter.
Could we remove it from the abbreviations set here?
@PatrickMassot advocated for this at Zulip
Impact
Add :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.