Best lim in unicode?

Stream: lean4

[Dean Young]

lim with an arrow under it is common throughout analysis and category theory as well.

I can't seem to find one in the unicode catalogue but maybe those combining characters like combining underscore and combining right arrow could make one: l + combining _ + i + combining _ + m + combining ->.

I'm trying to find the right combining characters as I write this.

Bonus if someone can get the arrow the other way.

[Jireh Loreaux]

li͢m

[Jireh Loreaux]

I think there is not a ← version though. This is U+0362 "Combining double rightwards arrow below"

[Dean Young]

I also made this:
l͟i͟m͟
if someone can find a > that goes under just nice it might work. I couldn't find one though.

[Dean Young]

Using U+0332 (combining low line)
U+20D7 (combining right arrow)
U+0362 (combining double rightwards arrow below)
U+035F

[Dean Young]

li͢m

[Dean Young]

l͟i͢m

[Dean Young]

those ones kinda suck.

[Eric Wieser]

I would claim that you don't actually want to use notation like this, because font and editor support for combining monospace characters is really bad

[Dean Young]

oh huh ... could come out completely different on a different platform.

[Eric Wieser]

If you want something pretty out of your lean code, you could define a ToLatex : Expr -> String function of some kind

[Dean Young]

Oh that seems fun.

[Eric Wieser]

I'm pretty certain that other people will have tried it, but I haven't seen anyone announce anything. I think it would be a good exercise to build something like that for basic algebra. Once you have that, sharing it might encourage people to share what they tried

[Reid Barton]

You could also sidestep the issue by writing "colim".

[Kyle Miller]

@Eric Wieser Here's a screenshot of something that's in the works (part of what Patrick talked about at IPAM), and it contains a LaTeX pretty printer for Expr:

image.png

(Nothing about finsets has really been refined yet. I just happened to be looking at how it handled Mathlib.Algebra.BigOperators.Basic.)

[Eric Wieser]

Yes, I just watched that talk; very cool!