Lean4
/-- The parser `subscript(term)` parses a subscript. Basic usage is:
```
local syntax:arg term:max subscript(term) : term
local macro_rules | `($a:term $i:subscript) => `($a $i)
```
Given a notation like this, the expression `(a)ᵢ` parses and expands to `a i`. (Either parentheses
or a whitespace as in `a ᵢ` is required, because `aᵢ` is considered as an identifier.)
Note that because of Unicode limitations, not many characters can actually be typed inside the
subscript, so this should not be used for complex expressions. Legal subscript characters:
```
₀₁₂₃₄₅₆₇₈₉ₐₑₕᵢⱼₖₗₘₙₒₚᵣₛₜᵤᵥₓᴀʙᴄᴅᴇꜰɢʜɪᴊᴋʟᴍɴᴏᴘꞯʀꜱᴛᴜᴠᴡʏᴢᵦᵧᵨᵩᵪ₊₋₌₍₎
```
-/
def subscript (p : Parser) : Parser :=
Superscript.scriptParser .subscript "subscript" "expected subscript character" p
