Documentation

Mathlib.Lean.Expr.Basic

Additional operations on Expr and related types #

This file defines basic operations on the types expr, name, declaration, level, environment.

This file is mostly for non-tactics.

Declarations about BinderInfo #

The brackets corresponding to a given BinderInfo.

Instances For

    Declarations about name #

    Find the largest prefix n of a Name such that f n != none, then replace this prefix with the value of f n.

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

      Build a name from components. For example from_components [`foo, `bar] becomes `foo.bar. It is the inverse of Name.components on list of names that have single components.

      Instances For

        Update the last component of a name.

        Instances For

          Get the last field of a name as a string. Doesn't raise an error when the last component is a numeric field.

          Instances For

            nm.splitAt n splits a name nm in two parts, such that the second part has depth n, i.e. (nm.splitAt n).2.getNumParts = n (assuming nm.getNumParts ≥ n). Example: splitAt `foo.bar.baz.back.bat 1 = (`foo.bar.baz.back, `bat).

            Instances For

              isPrefixOf? pre nm returns some post if nm = pre ++ post. Note that this includes the case where nm has multiple more namespaces. If pre is not a prefix of nm, it returns none.

              Equations
              Instances For

                Lean 4 makes declarations which are technically not internal (that is, head string does not start with _) but which sometimes should be treated as such. For example, the to_additive attribute needs to transform proof_1 constants generated by Lean.Meta.mkAuxDefinitionFor. This might be better fixed in core, but until then, this method can act as a polyfill. This method only looks at the name to decide whether it is probably internal. Note: this declaration also occurs as shouldIgnore in the Lean 4 file test/lean/run/printDecls.

                Instances For
                  def Lean.Name.isBlackListed {m : TypeType} [Monad m] [Lean.MonadEnv m] (declName : Lean.Name) :
                  Instances For

                    The union of two NameSets.

                    Instances For

                      Checks whether this ConstantInfo is a definition,

                      Instances For

                        Checks whether this ConstantInfo is a theorem,

                        Instances For

                          Update ConstantVal (the data common to all constructors of ConstantInfo) in a ConstantInfo.

                          Instances For

                            Update the name of a ConstantInfo.

                            Instances For

                              Update the type of a ConstantInfo.

                              Instances For

                                Update the level parameters of a ConstantInfo.

                                Instances For

                                  Update the value of a ConstantInfo, if it has one.

                                  Instances For

                                    Turn a ConstantInfo into a declaration.

                                    Instances For

                                      Same as mkConst, but with fresh level metavariables.

                                      Instances For

                                        Declarations about Expr #

                                        If the expression is a constant, return that name. Otherwise return Name.anonymous.

                                        Instances For

                                          Return the function (name) and arguments of an application.

                                          Instances For

                                            Like Expr.getUsedConstants, but produce a NameSet.

                                            Instances For

                                              Turn an expression that is a natural number literal into a natural number.

                                              Instances For

                                                Turn an expression that is a constructor of Int applied to a natural number literal into an integer.

                                                Instances For

                                                  Check if an expression is a "natural number in normal form", i.e. of the form OfNat n, where n matches .lit (.natVal lit) for some lit. and if so returns lit.

                                                  Instances For

                                                    Check if an expression is an "integer in normal form", i.e. either a natural number in normal form, or the negation of one, and if so returns the integer.

                                                    Instances For

                                                      Check if an expression is a "rational in normal form", i.e. either an integer number in normal form, or n / d where n is an integer in normal form, d is a natural number in normal form, d ≠ 1, and n and d are coprime (in particular, we check that (mkRat n d).den = d). If so returns the rational number.

                                                      Instances For

                                                        Test if an expression represents an explicit number written in normal form:

                                                        • A "natural number in normal form" is an expression OfNat.ofNat n, even if it is not of type , as long as n is a literal.
                                                        • An "integer in normal form" is an expression which is either a natural number in number form, or -n, where n is a natural number in normal form.
                                                        • A "rational in normal form" is an expressions which is either an integer in normal form, or n / d where n is an integer in normal form, d is a natural number in normal form, d ≠ 1, and n and d are coprime (in particular, we check that (mkRat n d).den = d).
                                                        Equations
                                                        Instances For

                                                          If an Expr has form .fvar n, then returns some n, otherwise none.

                                                          Instances For

                                                            isConstantApplication e checks whether e is syntactically an application of the form (fun x₁ ⋯ xₙ => H) y₁ ⋯ yₙ where H does not contain the variable xₙ. In other words, it does a syntactic check that the expression does not depend on yₙ.

                                                            Instances For

                                                              aux depth e n checks whether the body of the n-th lambda of e has loose bvar depth - 1.

                                                              Instances For

                                                                Counts the immediate depth of a nested let expression.

                                                                Equations
                                                                Instances For

                                                                  Check that an expression contains no metavariables (after instantiation).

                                                                  Instances For

                                                                    Construct the term of type α for a given natural number (doing typeclass search for the OfNat instance required).

                                                                    Instances For

                                                                      Construct the term of type α for a given integer (doing typeclass search for the OfNat and Neg instances required).

                                                                      Instances For

                                                                        Return some n if e is one of the following

                                                                        Test if an expression is either Nat.zero, or OfNat.ofNat 0.

                                                                        Instances For

                                                                          Tests is if an expression matches either x ≠ y or ¬ (x = y). If it matches, returns some (type, x, y).

                                                                          Instances For
                                                                            @[inline]

                                                                            Lean.Expr.le? e takes e : Expr as input. If e represents a ≤ b, then it returns some (t, a, b), where t is the Type of a, otherwise, it returns none.

                                                                            Instances For

                                                                              Given a proposition ty that is an Eq, Iff, or HEq, returns (tyLhs, lhs, tyRhs, rhs), where lhs : tyLhs and rhs : tyRhs, and where lhs is related to rhs by the respective relation.

                                                                              See also Lean.Expr.iff?, Lean.Expr.eq?, and Lean.Expr.heq?.

                                                                              Instances For
                                                                                def Lean.Expr.modifyAppArgM {M : TypeType u_1} [Functor M] [Pure M] (modifier : Lean.ExprM Lean.Expr) :
                                                                                Instances For
                                                                                  Instances For

                                                                                    Given f a₀ a₁ ... aₙ₋₁, runs modifier on the ith argument or returns the original expression if out of bounds.

                                                                                    Instances For

                                                                                      Given f a₀ a₁ ... aₙ₋₁, returns the ith argument or none if out of bounds.

                                                                                      Instances For
                                                                                        def Lean.Expr.modifyArgM {M : TypeType u_1} [Monad M] (modifier : Lean.ExprM Lean.Expr) (e : Lean.Expr) (i : Nat) (n : optParam Nat (Lean.Expr.getAppNumArgs e)) :

                                                                                        Given f a₀ a₁ ... aₙ₋₁, runs modifier on the ith argument. An argument n may be provided which says how many arguments we are expecting e to have.

                                                                                        Instances For

                                                                                          Traverses an expression e and renames bound variables named old to new.

                                                                                          Equations
                                                                                          Instances For

                                                                                            getBinderName e returns some n if e is an expression of the form ∀ n, ... and none otherwise.

                                                                                            Instances For

                                                                                              Annotates a binderIdent with the binder information from an fvar.

                                                                                              Instances For

                                                                                                If e has a structure as type with field fieldName, mkDirectProjection e fieldName creates the projection expression e.fieldName

                                                                                                Instances For

                                                                                                  If e has a structure as type with field fieldName (either directly or in a parent structure), mkProjection e fieldName creates the projection expression e.fieldName

                                                                                                  Instances For

                                                                                                    Returns true if e contains a name n where p n is true.

                                                                                                    Instances For

                                                                                                      Rewrites e via some eq, producing a proof e = e' for some e'.

                                                                                                      Rewrites with a fresh metavariable as the ambient goal. Fails if the rewrite produces any subgoals.

                                                                                                      Instances For

                                                                                                        Rewrites the type of e via some eq, then moves e into the new type via Eq.mp.

                                                                                                        Rewrites with a fresh metavariable as the ambient goal. Fails if the rewrite produces any subgoals.

                                                                                                        Instances For

                                                                                                          Return all names appearing in the type or value of a ConstantInfo.

                                                                                                          Instances For

                                                                                                            Get the projections that are projections to parent structures. Similar to getParentStructures, except that this returns the (last component of the) projection names instead of the parent names.

                                                                                                            Instances For

                                                                                                              Return the name of the module in which a declaration was defined.

                                                                                                              Instances For

                                                                                                                Return the names of the modules in which constants used in the specified declaration were defined.

                                                                                                                Note that this will not account for tactics and syntax used in the declaration, so the results may not suffice as imports.

                                                                                                                Instances For

                                                                                                                  Return the names of the modules in which constants used in the current file were defined.

                                                                                                                  Note that this will not account for tactics and syntax used in the file, so the results may not suffice as imports.

                                                                                                                  Instances For