## Stream: general

### Topic: Lean point

#### Sebastien Gouezel (Apr 02 2020 at 08:56):

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 (Apr 02 2020 at 08:59):

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

#### Johan Commelin (Apr 02 2020 at 09:01):

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

#### Yury G. Kudryashov (Apr 02 2020 at 11:16):

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

Last updated: May 15 2021 at 00:39 UTC