Lean4
/-- The parser `superscript(term)` parses a superscript. Basic usage is:
```
local syntax:arg term:max superscript(term) : term
local macro_rules | `($a:term $b:superscript) => `($a ^ $b)
```
Given a notation like this, the expression `2⁶⁴` parses and expands to `2 ^ 64`.
Note that because of Unicode limitations, not many characters can actually be typed inside the
superscript, so this should not be used for complex expressions. Legal superscript characters:
```
⁰¹²³⁴⁵⁶⁷⁸⁹ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ𐞥ʳˢᵗᵘᵛʷˣʸᶻᴬᴮᴰᴱᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾꟴᴿᵀᵁⱽᵂᵝᵞᵟᵋᶿᶥᶹᵠᵡ⁺⁻⁼⁽⁾
```
-/
def superscript (p : Parser) : Parser :=
Superscript.scriptParser .superscript "superscript" "expected superscript character" p
