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.

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

      Equations
      Instances For

        Update the last component of a name.

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

          Equations
          Instances For
            @[deprecated Lean.Name.lastComponentAsString]

            Alias of Lean.Name.lastComponentAsString.


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

            Equations
            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).

              Equations
              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
                  def Lean.Name.isBlackListed {m : TypeType} [Monad m] [Lean.MonadEnv m] (declName : Lean.Name) :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    Checks whether this ConstantInfo is a definition,

                    Equations
                    Instances For

                      Checks whether this ConstantInfo is a theorem,

                      Equations
                      Instances For

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

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

                          Update the name of a ConstantInfo.

                          Equations
                          • c.updateName name = c.updateConstantVal (let __src := c.toConstantVal; { name := name, levelParams := __src.levelParams, type := __src.type })
                          Instances For

                            Update the type of a ConstantInfo.

                            Equations
                            • c.updateType type = c.updateConstantVal (let __src := c.toConstantVal; { name := __src.name, levelParams := __src.levelParams, type := type })
                            Instances For

                              Update the level parameters of a ConstantInfo.

                              Equations
                              • c.updateLevelParams levelParams = c.updateConstantVal (let __src := c.toConstantVal; { name := __src.name, levelParams := levelParams, type := __src.type })
                              Instances For

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

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

                                  Turn a ConstantInfo into a declaration.

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

                                    Same as mkConst, but with fresh level metavariables.

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

                                      Declarations about Expr #

                                      Equations
                                      Instances For
                                        @[inline]

                                        Given f a b c, return #[f a, f a b, f a b c]. Each entry in the array is an Expr.app, and this array has the same length as the one returned by Lean.Expr.getAppArgs.

                                        Equations
                                        Instances For

                                          Erase proofs in an expression by replacing them with sorrys.

                                          This function replaces all proofs in the expression and in the types that appear in the expression by sorryAxs. The resulting expression has the same type as the old one.

                                          It is useful, e.g., to verify if the proof-irrelevant part of a definition depends on a variable.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          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.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            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.

                                                Equations
                                                Instances For

                                                  If an Expr has the form Type u, then return some u, otherwise none.

                                                  Equations
                                                  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ₙ.

                                                    Equations
                                                    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
                                                        • (Lean.Expr.letE declName type value b nonDep).letDepth = b.letDepth + 1
                                                        • x.letDepth = 0
                                                        Instances For

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

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

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

                                                            Equations
                                                            Instances For

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

                                                              Equations
                                                              Instances For

                                                                Return some n if e is one of the following

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

                                                                Equations
                                                                Instances For

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

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

                                                                    Equations
                                                                    • p.le? = do let __discrp.app4? `LE.le match __discr with | (type, fst, lhs, rhs) => pure (type, lhs, rhs)
                                                                    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?.

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For
                                                                        def Lean.Expr.modifyAppArgM {M : TypeType u} [Functor M] [Pure M] (modifier : Lean.ExprM Lean.Expr) :
                                                                        Equations
                                                                        Instances For
                                                                          Equations
                                                                          Instances For
                                                                            def Lean.Expr.modifyArg (modifier : Lean.ExprLean.Expr) (e : Lean.Expr) (i : Nat) (n : optParam Nat e.getAppNumArgs) :

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

                                                                            Equations
                                                                            Instances For
                                                                              def Lean.Expr.setArg (e : Lean.Expr) (i : Nat) (x : Lean.Expr) (n : optParam Nat e.getAppNumArgs) :

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

                                                                              Equations
                                                                              Instances For
                                                                                Equations
                                                                                • x✝.getRevArg? x = match x✝, x with | fn.app a, 0 => some a | f.app arg, i.succ => some (f.getRevArg! i) | x, x_1 => none
                                                                                Instances For
                                                                                  def Lean.Expr.getArg? (e : Lean.Expr) (i : Nat) (n : optParam Nat e.getAppNumArgs) :

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

                                                                                  Equations
                                                                                  • e.getArg? i n = e.getRevArg? (n - i - 1)
                                                                                  Instances For
                                                                                    def Lean.Expr.modifyArgM {M : TypeType u} [Monad M] (modifier : Lean.ExprM Lean.Expr) (e : Lean.Expr) (i : Nat) (n : optParam Nat e.getAppNumArgs) :

                                                                                    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.

                                                                                    Equations
                                                                                    Instances For

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

                                                                                      Equations
                                                                                      • (fn.app arg).renameBVar old new = (fn.renameBVar old new).app (arg.renameBVar old new)
                                                                                      • (Lean.Expr.lam n ty bd bi).renameBVar old new = Lean.Expr.lam (if (n == old) = true then new else n) (ty.renameBVar old new) (bd.renameBVar old new) bi
                                                                                      • (Lean.Expr.forallE n ty bd bi).renameBVar old new = Lean.Expr.forallE (if (n == old) = true then new else n) (ty.renameBVar old new) (bd.renameBVar old new) bi
                                                                                      • e.renameBVar old new = e
                                                                                      Instances For

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

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

                                                                                          Annotates a binderIdent with the binder information from an fvar.

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

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

                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            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

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

                                                                                                If e is a projection of the structure constructor, reduce the projection. Otherwise returns none. If this function detects that expression is ill-typed, throws an error. For example, given Prod.fst (x, y), returns some x.

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

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

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

                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    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.

                                                                                                      Equations
                                                                                                      Instances For

                                                                                                        Given (hNotEx : Not ex) where ex is of the form Exists x, p x, return a forall x, Not (p x) and a proof for it.

                                                                                                        This function handles nested existentials.

                                                                                                        Equations
                                                                                                        Instances For

                                                                                                          Given (hNotEx : Not (@Exists.{lvl} A p)), return a forall x, Not (p x) and a proof for it.

                                                                                                          This function handles nested existentials.

                                                                                                          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.

                                                                                                          Equations
                                                                                                          Instances For