Documentation

Mathlib.Mathport.Notation

The notation3 macro, simulating Lean 3's notation. #

Syntaxes supporting notation3 #

Expands binders into nested combinators. For example, the familiar exists is given by: expand_binders% (p => Exists p) x y : Nat, x < y which expands to the same expression as ∃ x y : Nat, x < y

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

        Keywording indicating whether to use a left- or right-fold.

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

          notation3 argument matching extBinders.

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

            notation3 argument simulating a Lean 3 fold notation.

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

              notation3 argument binding a name.

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

                notation3 argument.

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

                  Expression matching #

                  A more complicated part of notation3 is the delaborator generator. While notation relies on generating app unexpanders, we instead generate a delaborator directly so that we can control how binders are formatted (we want to be able to know the types of binders, whether a lambda is a constant function, and whether it is Prop-valued, which are not things we can answer once we pass to app unexpanders).

                  The dynamic state of a Matcher.

                  Instances For

                    The initial state.

                    Equations
                    Instances For

                      Evaluate f with the given variable's value as the SubExpr and within that subexpression's saved context. Fails if the variable has no value.

                      Equations
                      Instances For

                        Delaborate the given variable's value. Fails if the variable has no value. If checkNot is provided, then checks that the expression being delaborated is not the given one (this is used to prevent infinite loops).

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

                          Assign a variable to the current SubExpr, capturing the local context.

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

                            Get the accumulated array of delaborated terms for a given foldr/foldl. Returns #[] if nothing has been pushed yet.

                            Equations
                            • s.getFoldArray name = (s.foldState.find? name).getD #[]
                            Instances For
                              def Mathlib.Notation3.MatchState.getBinders (s : Mathlib.Notation3.MatchState) :
                              Array (Lean.TSyntax `Batteries.ExtendedBinder.extBinderParenthesized)

                              Get the accumulated array of delaborated terms for a given foldr/foldl. Returns #[] if nothing has been pushed yet.

                              Equations
                              • s.getBinders = s.scopeState.getD #[]
                              Instances For

                                Push a delaborated term onto a foldr/foldl array.

                                Equations
                                • s.pushFold name t = let ts := (s.getFoldArray name).push t; { vars := s.vars, scopeState := s.scopeState, foldState := s.foldState.insert name ts }
                                Instances For

                                  Matcher that assigns the current SubExpr into the match state; if a value already exists, then it checks for equality.

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

                                    Matcher for an expression satisfying a given predicate.

                                    Equations
                                    Instances For

                                      Matcher for Expr.fvar. It checks that the user name agrees and that the type of the expression is matched by matchTy.

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

                                        Matcher that checks that the type of the expression is matched by matchTy.

                                        Equations
                                        Instances For

                                          Matches raw nat lits.

                                          Equations
                                          Instances For

                                            Matches applications.

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

                                              Matches pi types. The name n should be unique, and matchBody should use n as the userName of its fvar.

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

                                                Matches lambdas. The matchBody takes the fvar introduced when visiting the body.

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

                                                  Adds all the names in boundNames to the local context with types that are fresh metavariables. This is used for example when initializing p in (scoped p => ...) when elaborating ....

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

                                                    Given an expression, generate a matcher for it. The boundFVars hash map records which state variables certain fvars correspond to. The localFVars hash map records which local variable the matcher should use for an exact expression match.

                                                    If it succeeds generating a matcher, returns

                                                    1. a list of keys that should be used for the delab attribute when defining the elaborator
                                                    2. a Term that represents a Matcher for the given expression e.

                                                    Returns a Term that represents a Matcher for the given pattern stx. The boundNames set determines which identifiers are variables in the pattern. Fails in the OptionT sense if it comes across something it's unable to handle.

                                                    Also returns constant names that could serve as a key for a delaborator. For example, if it's for a function f, then app.f.

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

                                                      Matcher for processing scoped syntax. Assumes the expression to be matched against is in the lit variable.

                                                      Runs smatcher, extracts the resulting scopeId variable, processes this value (which must be a lambda) to produce a binder, and loops.

                                                      Equations
                                                      Instances For

                                                        Variant of matchScoped after some number of binders have already been captured.

                                                        Create a Term that represents a matcher for scoped notation. Fails in the OptionT sense if a matcher couldn't be constructed. Also returns a delaborator key like in mkExprMatcher. Reminder: $lit:ident : (scoped $scopedId:ident => $scopedTerm:Term)

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

                                                          Matcher for expressions produced by foldl.

                                                          Create a Term that represents a matcher for foldl notation. Reminder: ( lit ","* => foldl (x y => scopedTerm) init)

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

                                                            Create a Term that represents a matcher for foldr notation. Reminder: ( lit ","* => foldr (x y => scopedTerm) init)

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

                                                              The notation3 command #

                                                              def Mathlib.Notation3.mkNameFromSyntax (name? : Option (Lean.TSyntax `Lean.Parser.Command.namedName)) (syntaxArgs : Array (Lean.TSyntax `stx)) (attrKind : Lean.TSyntax `Lean.Parser.Term.attrKind) :

                                                              Create a name that we can use for the syntax definition, using the algorithm from notation.

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

                                                                Used when processing different kinds of variables when building the final delaborator.

                                                                Instances For
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    def Mathlib.Notation3.getPrettyPrintOpt (opt? : Option (Lean.TSyntax `Mathlib.Notation3.prettyPrintOpt)) :

                                                                    Interpret a prettyPrintOpt. The default value is true.

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

                                                                      notation3 declares notation using Lean-3-style syntax.

                                                                      Examples:

                                                                      notation3 "∀ᶠ " (...) " in " f ", " r:(scoped p => Filter.eventually p f) => r
                                                                      notation3 "MyList[" (x", "* => foldr (a b => MyList.cons a b) MyList.nil) "]" => x
                                                                      

                                                                      By default notation is unable to mention any variables defined using variable, but local notation3 is able to use such local variables.

                                                                      Use notation3 (prettyPrint := false) to keep the command from generating a pretty printer for the notation.

                                                                      This command can be used in mathlib4 but it has an uncertain future and was created primarily for backward compatibility.

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

                                                                        scoped[ns] support