This is broken now as I merged the other lean change. Would you mind rebasing this?

At some point there might be a push to make `lean` refer to Lean 4.
This is consistent with how `python2` is used for Python 2 code.

Looks good, but could you also add a definition Lean3Lexer = LeanLexer?

@jeanas: does the commit I just pushed look ok?

Almost — __all__ should still contain LeanLexer.

Done; this results in the mapping file being updated too, but I guess that's ok?

Adding such an alias to __all__ breaks the test. I could switch to class LeanLexer(Lean3Lexer): pass if you prefer?

Yes, it's ok. However, it now complains that there are several conflicting lexers for the same file types. Never mind, I'll fix it.