Lean point

Stream: general

[Sebastien Gouezel]

Do you get a Lean point when, typing a paper in latex, you use Lean commands instead of latex ones (and of course latex complains that this is nonsense to use \comp for composition)? Maybe the next move is to have a preamble in my latex files converting all Lean commands to latex commands.

[Kevin Buzzard]

I get $ and $$ mixed up because of TeX v this chat.

[Johan Commelin]

The move after the next move will be a tactic command #export_to_latex

[Yury G. Kudryashov]

I use lean emacs input mode to typeset Unicode characters, then compile with lualatex. I also have a sed script that creates a non-unicode version for arxiv and journals