A parser for superscripts and subscripts

This is intended for use in local notations. Basic usage is:

local syntax:arg term:max superscript(term) : term
local macro_rules | `($a:term $b:superscript) => `($a ^ $b)

where superscript(term) indicates that it will parse a superscript, and the $b:superscript antiquotation binds the term argument of the superscript. Given a notation like this, the expression 2⁶⁴ parses and expands to 2 ^ 64.

The superscript body is considered to be the longest contiguous sequence of superscript tokens and whitespace, so no additional bracketing is required (unless you want to separate two superscripts). However, note that Unicode has a rather restricted character set for superscripts and subscripts (see Mapping.superscript and Mapping.subscript in this file), so you should not use this parser for complex expressions.

@[implicit_reducible]

instance Mathlib.Tactic.Superscript.instHashableChar_mathlib : Hashable Char

structure Mathlib.Tactic.Superscript.Mapping : Type

A bidirectional character mapping.

• toNormal : Std.HashMap Char Char

  Map from "special" (e.g. superscript) characters to "normal" characters.

• toSpecial : Std.HashMap Char Char

  Map from "normal" text to "special" (e.g. superscript) characters.

@[implicit_reducible]

instance Mathlib.Tactic.Superscript.instInhabitedMapping : Inhabited Mapping

def Mathlib.Tactic.Superscript.instInhabitedMapping.default : Mapping

def Mathlib.Tactic.Superscript.mkMapping (s₁ s₂ : String) : Mapping

Constructs a mapping (intended for compile time use). Panics on violated invariants.

def Mathlib.Tactic.Superscript.Mapping.superscript : Mapping

A mapping from superscripts to and from regular text.

def Mathlib.Tactic.Superscript.Mapping.subscript : Mapping

A mapping from subscripts to and from regular text.

def Mathlib.Tactic.Superscript.satisfyTokensFn (p : Char → Bool) (errorMsg : String) (many : Bool := true) (k : Array (String.Pos.Raw × String.Pos.Raw × String.Pos.Raw) → Lean.Parser.ParserState → Lean.Parser.ParserState) : Lean.Parser.ParserFn

Collects runs of text satisfying p followed by whitespace. Fails if the first character does not satisfy p. If many is true, it will parse 1 or more many whitespace-separated runs, otherwise it will parse only 1. If successful, it passes the result to k as an array (a, b, c) where a..b is a token and b..c is whitespace.

@[irreducible, specialize #[]]

def Mathlib.Tactic.Superscript.partitionPoint {α : Type u} [Inhabited α] (as : Array α) (leftOfPartition : α → Bool) (lo : ℕ := 0) (hi : ℕ := as.size) : ℕ

Given a predicate leftOfPartition which is true for indexes < i and false for ≥ i, returns i, by binary search.

def Mathlib.Tactic.Superscript.scriptFnNoAntiquot (m : Mapping) (errorMsg : String) (p : Lean.Parser.ParserFn) (many : Bool := true) : Lean.Parser.ParserFn

The core function for super/subscript parsing. It consists of three stages:

1. Parse a run of superscripted characters, skipping whitespace and stopping when we hit a non-superscript character.
2. Un-superscript the text and pass the body to the inner parser (usually term).
3. Take the resulting Syntax object and align all the positions to fit back into the original text (which as a side effect also rewrites all the substrings to be in subscript text).

If many is false, then whitespace (and comments) are not allowed inside the superscript.

def Mathlib.Tactic.Superscript.scriptParser (m : Mapping) (antiquotName errorMsg : String) (p : Lean.Parser.Parser) (many : Bool := true) (kind : Lean.SyntaxNodeKind := by exact decl_name%) : Lean.Parser.Parser

The super/subscript parser.

• m: the character mapping
• antiquotName: the name to use for antiquotation bindings $a:antiquotName. Note that the actual syntax kind bound will be the body kind (parsed by p), not kind.
• errorMsg: shown when the parser does not match
• p: the inner parser (usually term), to be called on the body of the superscript
• many: if false, whitespace is not allowed inside the superscript
• kind: the term will be wrapped in a node with this kind; generally this is a name of the parser declaration itself.

def Mathlib.Tactic.Superscript.scriptParser.parenthesizer (k : Lean.SyntaxNodeKind) (p : Lean.PrettyPrinter.Parenthesizer) : Lean.PrettyPrinter.Parenthesizer

Parenthesizer for the script parser.

def Std.Format.mapStringsM {m : Type → Type u_1} [Monad m] (f : Format) (f' : String → m String) : m Format

Map over the strings in a Format.

def Mathlib.Tactic.Superscript.scriptParser.formatter (name : String) (m : Mapping) (k : Lean.SyntaxNodeKind) (p : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Formatter for the script parser.

def Mathlib.Tactic.superscript (p : Lean.Parser.Parser) : Lean.Parser.Parser

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 Mathlib.Tactic.superscript.parenthesizer (p : Lean.PrettyPrinter.Parenthesizer) : Lean.PrettyPrinter.Parenthesizer

Formatter for the superscript parser.

def Mathlib.Tactic.superscript.formatter (p : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Formatter for the superscript parser.

def Mathlib.Tactic.superscriptTerm : Lean.Parser.Parser

Shorthand for superscript(term).

This is needed because the initializer below does not always run, and if it has not run then downstream parsers using the combinators will crash.

See https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Non-builtin.20parser.20aliases/near/365125476 for some context.

def Mathlib.Tactic.subscript (p : Lean.Parser.Parser) : Lean.Parser.Parser

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 Mathlib.Tactic.subscript.parenthesizer (p : Lean.PrettyPrinter.Parenthesizer) : Lean.PrettyPrinter.Parenthesizer

Formatter for the subscript parser.

def Mathlib.Tactic.subscript.formatter (p : Lean.PrettyPrinter.Formatter) : Lean.PrettyPrinter.Formatter

Formatter for the subscript parser.

def Mathlib.Tactic.subscriptTerm : Lean.Parser.Parser

Shorthand for subscript(term).

This is needed because the initializer below does not always run, and if it has not run then downstream parsers using the combinators will crash.

See https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Non-builtin.20parser.20aliases/near/365125476 for some context.

def Mathlib.Tactic.delabSuperscript : Lean.PrettyPrinter.Delaborator.Delab

Successfully delaborates only if the resulting expression can be superscripted.

See Mapping.superscript in this file for legal superscript characters.

def Mathlib.Tactic.delabSubscript : Lean.PrettyPrinter.Delaborator.Delab

Successfully delaborates only if the resulting expression can be subscripted.

See Mapping.subscript in this file for legal subscript characters.