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

                                  Turn a ConstantInfo into a declaration.

                                  Equations
                                  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

                                            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
                                                                  @[inline]

                                                                  Lean.Expr.lt? 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.lt? = do let __discrp.app4? `LT.lt 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
                                                                              • (fn.app a).getRevArg? 0 = some a
                                                                              • (f.app arg).getRevArg? i.succ = some (f.getRevArg! i)
                                                                              • x✝.getRevArg? x = 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