Lean LaTeX utf8 v utf8x

Stream: general

[Kevin Buzzard]

I am writing an article for the London Maths Society and I'm using their style file, which has the line
\RequirePackage[utf8]{inputenc}. This means that TeX chokes when I write the line \usepackage[utf8x]{inputenc} as in the sample file. If I instead use utf8 then my Lean code breaks, because the characters α → β ↔ ∀ \< \>don't get interpreted correctly (most of them become exists or lambda).

Is there some workaround for this (e.g. manually editing my code), before I start complaining to the journal that their style file clashes with Lean's set-up for quoting code?

[Johan Commelin]

That sounds painful... I don't know of any workaround

[Wojciech Nawrocki]

You can do this:

\usepackage{newunicodechar}
\newfontfamily{\freeserif}[Scale=MatchLowercase]{DejaVu Sans} % This font has to be one that supports Unicode
\newunicodechar{λ}{{\freeserif{λ}}}
\newunicodechar{ℕ}{{\freeserif{ℕ}}}
\newunicodechar{ₐ}{{\freeserif{ₐ}}}
\newunicodechar{₁}{{\freeserif{₁}}}
% etc

That said, I think this might require LuaLatex to build, but it's worth a try.

[Kevin Buzzard]

Oh thanks for this Wojciech! I was wondering if there might be a workaround of this nature.