superscript parser

Stream: mathlib4

[Mario Carneiro]

import Mathlib.Util.Superscript

macro a:term b:superscript(term) : term => `($a ^ $(⟨b.raw[0]⟩))

example : 2² = 4 := rfl
example : 2¹⁶ = 65536 := rfl
example : (fun n => 2ⁿ⁺¹) 15 = 2¹⁶ := rfl

[Mario Carneiro]

not yet PR'd, but it basically works as pictured

[Mario Carneiro]

you can even ctrl click the ⁿ to go to the binding site of the fun n =>

[Henrik Böving]

But not all unicode characters can be superscripted can they? Or was that subscripted. I can clearly remember that not even all numbers could be super or subscripted I just don't remember which it was.

[Mario Carneiro]

that's right, so you can only spell some words or use some symbols in the subscript

[Mario Carneiro]

there is also a subscript parser

[Mario Carneiro]

my plan is to make the parser available in mathlib but not actually use it globally, and let people use it in local notations when it makes sense

[Henrik Böving]

Hm, I'm not sure if it is good to further splitting up notation style with this because we can but if the majority likes it go for it :thumbs_up:

[Mario Carneiro]

what do you mean by that?

[Henrik Böving]

Well with this we are once again handing out yet another option to write quite literally the same thing (something that is already possible in base Lean already, for example inductive types can be denote with and without where if you wish) just because it is possible, I don't really see the advantage of having it done like this. I guess it looks nice and more familiar?

I just generally believe that with Lean already being as rich in syntax as it is we should try to stick to one way to write the same thing.

[Mario Carneiro]

Local notations which do this kind of thing already exist in mathlib, for example defining ℝⁿ⁺¹ to mean Fin (n + 1) -> ℝ for some local variable named n

[Mario Carneiro]

I'm not sure what you mean by "literally the same thing", it's a macro (which you can think of as a notation in this case) which lets you write the same thing you could before but with different syntax

[Mario Carneiro]

that's kind of the point

[Mario Carneiro]

(Just to be clear, I have no intention of using this for the power function on Nat. That was just a demo.)

[Mario Carneiro]

Henrik Böving said:

But not all unicode characters can be superscripted can they? Or was that subscripted. I can clearly remember that not even all numbers could be super or subscripted I just don't remember which it was.

Actually both are incomplete. Here are the defined mappings:

def Mapping.superscript := mkMapping
  "⁰¹²³⁴⁵⁶⁷⁸⁹ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ𐞥ʳˢᵗᵘᵛʷˣʸᶻᴬᴮᴰᴱᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾꟴᴿᵀᵁⱽᵂᵝᵞᵟᵋᶿᶥᶹᵠᵡ⁺⁻⁼⁽⁾"
  "0123456789abcdefghijklmnopqrstuvwxyzABDEGHIJKLMNOPQRTUVWβγδεθιυφχ+-=()"

def Mapping.subscript := mkMapping
  "₀₁₂₃₄₅₆₇₈₉ₐₑₕᵢⱼₖₗₘₙₒₚᵣₛₜᵤᵥₓᴀʙᴄᴅᴇꜰɢʜɪᴊᴋʟᴍɴᴏᴘꞯʀꜱᴛᴜᴠᴡʏᴢᵦᵧᵨᵩᵪ₊₋₌₍₎"
  "0123456789aehijklmnoprstuvxABCDEFGHIJKLMNOPQRSTUVWYZβγρφχ+-=()"

[Mario Carneiro]

you don't even have *, which makes it kind of hard to write formulas

[James Gallicchio]

those feel so arbitrary... unicode weirdness??

[Mario Carneiro]

it's because different parts of the alphabet were introduced at different times for different reasons

[Mario Carneiro]

if you look at the codepoint values they are all over the place

[Eric Wieser]

This mkMapping API seems nice in principle ("oh, the columns will align"), but the reality is:

image.png
image.png

[Eric Wieser]

It looks like (white screenshot) Microsoft rather dropped the ball on Consolas subscript characters (maybe that's fixed in newer versions than the one I have?)

[Henrik Böving]

I once spend two days figuring out the font with the most monospaced unicode characters to use with Lean, my decision at the time was julia mono:
image.png
i would say it is holding up pretty well

[Eric Wieser]

Though Zulip's "Source Code Pro" default has even fewer characters

[Eric Wieser]

@Henrik Böving, very weird that the only failing subscript is a capital F

[Damiano Testa]

Also, what's up with the q?

[Henrik Böving]

It seems like it doesnt exist in julia mono, if you look at marios thing above for me the q looks very weird as well

[Henrik Böving]

Maybe the q is new?

[Eric Wieser]

The q is not a true superscript character

[Eric Wieser]

It's https://unicode-explorer.com/c/107A5

[Henrik Böving]

"modifier letter small q" who comes up with this

[Eric Wieser]

I mean it's IPA

[Eric Wieser]

Unicode is supposed to be semantic not visual

[Mario Carneiro]

I think that character only theoretically exists. I put it in for completeness but I have not seen any font render it as not a box

[Mario Carneiro]

at least the julia font renders the capital Q, mine doesn't

[Mario Carneiro]

!4#4957

[Mario Carneiro]

Hm, now here's an interesting edge case:

#check 2² ⁻⁻ᶠᵒᵒ + 2
-- 2 ^ 2 + 2 : Nat

[Mario Carneiro]

oh my...

#check 2² ⁻⁻ /-
- 2 --/ + 2

-- 2 ^ (2 - 2) + 2 : Nat

you can comment out comments :mind_blown: