Zulip Chat Archive

Stream: general

Topic: Lean point

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Apr 02 2020 at 08:59):

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

view this post on Zulip Johan Commelin (Apr 02 2020 at 09:01):

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

view this post on Zulip 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