Topic: parsing LaTeX
Kevin Buzzard (Jun 19 2021 at 13:48):
Can I make this parse by telling a parser to "ignore the stupid mathematician and their LaTeX, just parse $\ell$ it as
l or even better "just parse $\ell\ne p$ as
l ≠ p. I'm quite happy to use "math
$", some easy-to-type unicode variant of
$ which we tell mathematicians to use if they want to do LaTeX in Lean 4 or whatever?
Last updated: Aug 03 2023 at 10:10 UTC