Documentation

Lean.PrettyPrinter.Delaborator.Builtins

If cond is true, wraps the syntax produced by d in a type ascription.

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

    Wraps the identifier (or identifier with explicit universe levels) with @ if pp.analysis.blockImplicit is set to true.

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

              Delaborator for const expressions. This is not registered as a delaborator, as const is not an expression kind (see [delab] description and Lean.PrettyPrinter.Delaborator.getExprKind). Rather, it is called through the app delaborator.

              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

                  A structure that records details of a function parameter.

                  • name : Lake.Name

                    Binder name for the parameter.

                  • Binder info for the parameter.

                  • defVal : Option Lean.Expr

                    The default value for the parameter, if the parameter has a default value.

                  • isAutoParam : Bool

                    Whether the parameter is an autoparam (i.e., whether it uses a tactic for the default value).

                  Instances For
                    Equations

                    Returns true if the parameter is an explicit parameter that has neither a default value nor a tactic.

                    Equations
                    • param.isRegularExplicit = (param.bInfo.isExplicit && !param.isAutoParam && param.defVal.isNone)
                    Instances For

                      Given a function f supplied with arguments args, returns an array whose n-th element is set to the kind of the n-th argument's associated parameter. We do not assume the expression mkAppN f args is sensical, and this function captures errors (except for panics) and returns the empty array in that case.

                      The returned array might be longer than the number of arguments. It gives parameter kinds for the fully-applied function. Note: the defVal expressions are only guaranteed to be valid for parameters associated to the supplied arguments; after this, they might refer to temporary fvars.

                      This function properly handles "overapplied" functions. For example, while id takes one explicit argument, it can take more than one explicit argument when its arguments are specialized to function types, like in id id 2.

                      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

                          Takes application syntax and converts it into structure instance notation, if possible. Assumes that the application is pretty printed in implicit mode.

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

                            If e is an application that is a candidate for using field notation, returns the parameter index and the field name to use. Checks that there are enough arguments.

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

                              In explicit mode, decides whether or not the applied function needs @, where numArgs is the number of arguments actually supplied to f.

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

                                Delaborates a function application in explicit mode.

                                • If insertExplicit is true, then ensures the head syntax is wrapped with @.
                                • If fieldNotation is true, then allows the application to be pretty printed using field notation. Field notation will not be used when insertExplicit is true.
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  Records how a particular argument to a function is delaborated, in non-explicit mode.

                                  Instances For

                                    Whether unexpanding is allowed with this argument.

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

                                      If the argument has associated syntax, returns it.

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

                                        Delaborates a function application in the standard mode, where implicit arguments are generally not included, unless pp.analysis.namedArg is set at that argument.

                                        This delaborator is where app_unexpanders and the structure instance unexpander are applied, if unexpand is true. When unexpand is true, also considers opportunities for field notation, which takes priority over other unexpanders.

                                        Assumes numArgs ≤ paramKinds.size.

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

                                          Delaborates the current argument. The argument remainingArgs is the number of arguments in the application after this one.

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

                                            Runs the given unexpanders, returning the resulting syntax if any are applicable, and otherwise fails.

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

                                              If the expression is a candidate for app unexpanders, try applying an app unexpander using some prefix of the arguments, longest prefix first. This function makes sure that the unexpanded syntax is annotated and given TermInfo so that it is hoverable in the InfoView.

                                              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

                                                  Returns true if an application should use explicit mode when delaborating. Explicit mode turns off unexpanders

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

                                                    Delaborates applications. Removes up to maxArgs arguments to form the "head" of the application.

                                                    • delabHead is a delaborator to use for the head of the expression. It is passed whether the result needs to have @ inserted.
                                                    • If unexpand is true, then allow unexpanders and field notation. This should likely be set to false except in the main delabApp delaborator.

                                                    Propagates pp.tagAppFns into the head for delabHead.

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

                                                      Default delaborator for applications.

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

                                                        The withOverApp combinator allows delaborators to handle "over-application" by using the core application delaborator to handle additional arguments.

                                                        For example, suppose f : {A : Type} → Foo A → A and we want to implement a delaborator for applications f x to pretty print as F[x]. Because A is a type variable we might encounter a term of the form @f (A → B) x y, which has an additional argument y. With this combinator one can use an arity-2 delaborator to pretty print this as F[x] y.

                                                        • arity: the expected number of arguments to f. The combinator will fail if fewer than this number of arguments are passed, and if more than this number of arguments are passed the arguments are handled using the standard application delaborator.
                                                        • x: delaborates the head application of the expected arity (f x in the example). The value of pp.tagAppFns for the whole application is propagated to the expression that x sees.

                                                        In the event of overapplication, the delaborator x is wrapped in Lean.PrettyPrinter.Delaborator.withAnnotateTermInfo to register TermInfo for the resulting term. The effect of this is that the term is hoverable in the Infoview.

                                                        If the application would require inserting @ around the result of x, the delaborator fails since we cannot be sure that this insertion will be well-formed.

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

                                                          State for delabAppMatch and helpers.

                                                          • matcherTy : Lean.SubExpr

                                                            The matcherTy instantiated with universe levels and the matcher parameters, with a position at the type of this application prefix.

                                                          • The motive, with the pi type version delaborated and the original expression version. Once AppMatchState is complete, this is not none.

                                                          • motiveNamed : Bool

                                                            Whether pp.analysis.namedArg was set for the motive argument.

                                                          • discrs : Array Lean.Term

                                                            The delaborated discriminants, without h : annotations.

                                                          • hNames? : Array (Option Lake.Name)

                                                            The collection of names used for the h : discriminant annotations, in order. Uniquified names are constructed after the first phase.

                                                          • Lambda subexpressions for each alternate.

                                                          • varNames : Array (Array Lake.Name)

                                                            For each match alternative, the names to use for the pattern variables. Each ends with hNames?.filterMap id exactly.

                                                          • The delaborated right-hand sides for each match alternative.

                                                          Instances For

                                                            Delaborates applications of "matchers" such as

                                                            List.map.match_1 : {α : Type _} →
                                                              (motive : List α → Sort _) →
                                                                (x : List α) → (Unit → motive List.nil) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
                                                            
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For

                                                              Adds hNames to the local context to reserve their names and runs m in that context.

                                                              Delaborates applications of the form letFun v (fun x => b) as let_fun x := v; b.

                                                              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

                                                                  Check for a Syntax.ident of the given name anywhere in the tree. This is usually a bad idea since it does not check for shadowing bindings, but in the delaborator we assume that bindings are never shadowed.

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

                                                                            Core function that delaborates a natural number (an OfNat.ofNat literal).

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

                                                                              Core function that delaborates a negative integer literal (a Neg.neg applied to OfNat.ofNat).

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

                                                                                Core function that delaborates a rational literal that is the division of an integer literal by a natural number literal. The division must be homogeneous for it to count as a rational literal.

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

                                                                                  Delaborates an OfNat.ofNat literal. @OfNat.ofNat _ n _ ~> n.

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

                                                                                    Delaborates the negative of an OfNat.ofNat literal. -@OfNat.ofNat _ n _ ~> -n

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

                                                                                      Delaborates a rational number literal. @OfNat.ofNat _ n _ / @OfNat.ofNat _ m ~> n / m and -@OfNat.ofNat _ n _ / @OfNat.ofNat _ m ~> -n / m

                                                                                      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

                                                                                          Delaborate a projection primitive. These do not usually occur in user code, but are pretty-printed when e.g. #printing a projection function.

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

                                                                                            This delaborator tries to elide functions which are known coercions. For example, Int.ofNat is a coercion, so instead of printing ofNat n we just print ↑n, and when re-parsing this we can (usually) recover the specific coercion being used.

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

                                                                                                              Pretty-prints a constant c as c.{<levels>} <params> : <type>.

                                                                                                              If universes is false, then the universe level parameters are omitted.

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

                                                                                                                Inner loop for delabParams, collecting binders. Invariants:

                                                                                                                • The current expression is a forall.
                                                                                                                • It has a name that's not inaccessible.
                                                                                                                • It has a name that hasn't been used yet.
                                                                                                                Equations
                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                Instances For