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.

instance Mathlib.Tactic.Superscript.instHashableChar : Hashable Char

structure Mathlib.Tactic.Superscript.Mapping : Type

• toNormal : Lean.HashMap Char Char

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

• toSpecial : Lean.HashMap Char Char

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

A bidirectional character mapping.

instance Mathlib.Tactic.Superscript.instInhabitedMapping : Inhabited Mathlib.Tactic.Superscript.Mapping

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

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

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

A mapping from superscripts to and from regular text.

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

A mapping from subscripts to and from regular text.

def Mathlib.Tactic.Superscript.satisfyTokensFn (p : Char → Bool) (errorMsg : String) (many : optParam Bool true) (k : Array (String.Pos × String.Pos × String.Pos) → 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.

partial def Mathlib.Tactic.Superscript.satisfyTokensFn.loop (p : Char → Bool) (k : Array (String.Pos × String.Pos × String.Pos) → Lean.Parser.ParserState → Lean.Parser.ParserState) (c : Lean.Parser.ParserContext) (toks : Array (String.Pos × String.Pos × String.Pos)) (s : Lean.Parser.ParserState) : Lean.Parser.ParserState

Loop body of satisfyTokensFn

@[specialize #[]]

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

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 : Mathlib.Tactic.Superscript.Mapping) (errorMsg : String) (p : Lean.Parser.ParserFn) (many : optParam 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.scriptFnNoAntiquot.align (aligns : Array (String.Pos × String.Pos)) (pos : String.Pos) : String.Pos

Applies the alignment mapping to a position.

def Mathlib.Tactic.Superscript.scriptFnNoAntiquot.alignSubstr (input : String) (aligns : Array (String.Pos × String.Pos)) : Substring → Substring

Applies the alignment mapping to a Substring.

def Mathlib.Tactic.Superscript.scriptFnNoAntiquot.alignInfo (input : String) (aligns : Array (String.Pos × String.Pos)) : Lean.SourceInfo → Lean.SourceInfo

Applies the alignment mapping to a SourceInfo.

partial def Mathlib.Tactic.Superscript.scriptFnNoAntiquot.alignSyntax (input : String) (aligns : Array (String.Pos × String.Pos)) : Lean.Syntax → Lean.Syntax

Applies the alignment mapping to a Syntax.

def Mathlib.Tactic.Superscript.scriptParser (m : Mathlib.Tactic.Superscript.Mapping) (antiquotName : String) (errorMsg : String) (p : Lean.Parser.Parser) (many : optParam Bool true) (kind : autoParam Lean.SyntaxNodeKind _auto✝) : 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

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

Parenthesizer for the script parser.

def Mathlib.Tactic.Superscript.scriptParser.formatter (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.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.registerAliasCore {α : Type} (mapRef : IO.Ref (Lean.Parser.AliasTable α)) (aliasName : Lean.Name) (value : Lean.Parser.AliasValue α) : IO Unit

def Mathlib.Tactic.registerAlias (aliasName : Lean.Name) (declName : Lean.Name) (p : Lean.Parser.ParserAliasValue) (kind? : optParam (Option Lean.SyntaxNodeKind) none) (info : optParam Lean.Parser.ParserAliasInfo { declName := Lean.Name.anonymous, stackSz? := some 1, autoGroupArgs := Option.isSome (some 1) }) : IO Unit