Documentation

Mathlib.Util.Superscript

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.

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.

Instances For

    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.
    Instances For

      A mapping from superscripts to and from regular text.

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

        A mapping from subscripts to and from regular text.

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

          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.
          Instances For
            @[irreducible, specialize #[]]
            def Mathlib.Tactic.Superscript.partitionPoint {α : Type u} [Inhabited α] (as : Array α) (leftOfPartition : αBool) (lo : optParam Nat 0) (hi : optParam Nat as.size) :

            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.
            Instances For

              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.
              Instances For

                Applies the alignment mapping to a position.

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

                  Applies the alignment mapping to a Substring.

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

                    Applies the alignment mapping to a SourceInfo.

                    Equations
                    Instances For

                      Applies the alignment mapping to a Syntax.

                      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.
                      Instances For
                        def Std.Format.mapStringsM {m : TypeType u_1} [Monad m] (f : Lean.Format) (f' : Stringm String) :

                        Map over the strings in a Format.

                        Equations
                        Instances For

                          Formatter for the script parser.

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

                            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.
                            Instances For

                              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
                              Instances For