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_mathlib : Hashable Char

Equations

• Mathlib.Tactic.Superscript.instHashableChar_mathlib = { hash := fun (c : Char) => hash c.val }

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.

instance Mathlib.Tactic.Superscript.instInhabitedMapping : Inhabited Mapping

Equations

• Mathlib.Tactic.Superscript.instInhabitedMapping = { default := { toNormal := default, toSpecial := default } }

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

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

Equations

• One or more equations did not get rendered due to their size.

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

A mapping from superscripts to and from regular text.

Equations

• One or more equations did not get rendered due to their size.

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

A mapping from subscripts to and from regular text.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

@[irreducible, specialize #[]]

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

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Superscript.scriptFnNoAntiquot.align (aligns : Array (String.Pos × String.Pos)) (pos : String.Pos) : String.Pos

Applies the alignment mapping to a position.

Equations

• One or more equations did not get rendered due to their size.

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

Applies the alignment mapping to a Substring.

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Superscript.scriptFnNoAntiquot.alignInfo input aligns Lean.SourceInfo.none = Lean.SourceInfo.none

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 : 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

Equations

• One or more equations did not get rendered due to their size.

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

Parenthesizer for the script parser.

Equations

• Mathlib.Tactic.Superscript.scriptParser.parenthesizer k p = Lean.PrettyPrinter.Parenthesizer.node.parenthesizer k p

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.

Equations

• (f_2.group b).mapStringsM f' = (fun (x : Std.Format) => x.group b) <$> f_2.mapStringsM f'
• (Std.Format.tag t g).mapStringsM f' = Std.Format.tag t <$> g.mapStringsM f'
• (f_2.append g).mapStringsM f' = Std.Format.append <$> f_2.mapStringsM f' <*> g.mapStringsM f'
• (Std.Format.nest n f_2).mapStringsM f' = Std.Format.nest n <$> f_2.mapStringsM f'
• (Std.Format.text s).mapStringsM f' = Std.Format.text <$> f' s
• (Std.Format.align force).mapStringsM f' = pure (Std.Format.align force)
• Std.Format.line.mapStringsM f' = pure Std.Format.line
• Std.Format.nil.mapStringsM f' = pure Std.Format.nil

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.

Equations

• One or more equations did not get rendered due to their size.

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:

⁰¹²³⁴⁵⁶⁷⁸⁹ᵃᵇᶜᵈᵉᶠᵍʰⁱʲᵏˡᵐⁿᵒᵖ𐞥ʳˢᵗᵘᵛʷˣʸᶻᴬᴮᴰᴱᴳᴴᴵᴶᴷᴸᴹᴺᴼᴾꟴᴿᵀᵁⱽᵂᵝᵞᵟᵋᶿᶥᶹᵠᵡ⁺⁻⁼⁽⁾

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.superscript.parenthesizer (p : Lean.PrettyPrinter.Parenthesizer) : Lean.PrettyPrinter.Parenthesizer

Formatter for the superscript parser.

Equations

• Mathlib.Tactic.superscript.parenthesizer = Mathlib.Tactic.Superscript.scriptParser.parenthesizer `Mathlib.Tactic.superscript

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

Formatter for the superscript parser.

Equations

• Mathlib.Tactic.superscript.formatter = Mathlib.Tactic.Superscript.scriptParser.formatter "superscript" Mathlib.Tactic.Superscript.Mapping.superscript `Mathlib.Tactic.superscript

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.

Equations

• One or more equations did not get rendered due to their size.

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:

₀₁₂₃₄₅₆₇₈₉ₐₑₕᵢⱼₖₗₘₙₒₚᵣₛₜᵤᵥₓᴀʙᴄᴅᴇꜰɢʜɪᴊᴋʟᴍɴᴏᴘꞯʀꜱᴛᴜᴠᴡʏᴢᵦᵧᵨᵩᵪ₊₋₌₍₎

Equations

• Mathlib.Tactic.subscript p = Mathlib.Tactic.Superscript.scriptParser Mathlib.Tactic.Superscript.Mapping.subscript "subscript" "expected subscript character" p true `Mathlib.Tactic.subscript

def Mathlib.Tactic.subscript.parenthesizer (p : Lean.PrettyPrinter.Parenthesizer) : Lean.PrettyPrinter.Parenthesizer

Formatter for the subscript parser.

Equations

• Mathlib.Tactic.subscript.parenthesizer = Mathlib.Tactic.Superscript.scriptParser.parenthesizer `Mathlib.Tactic.subscript

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

Formatter for the subscript parser.

Equations

• Mathlib.Tactic.subscript.formatter = Mathlib.Tactic.Superscript.scriptParser.formatter "subscript" Mathlib.Tactic.Superscript.Mapping.subscript `Mathlib.Tactic.subscript

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.

Equations

• One or more equations did not get rendered due to their size.