Documentation

Std.Lean.Expr

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.

Converts an Expr into a Syntax, by creating a fresh metavariable assigned to the expr and returning a named metavariable syntax ?a.

Instances For

    Returns the number of leading binders of an expression. Ignores metadata.

    Equations
    Instances For

      Returns the number of leading λ binders of an expression. Ignores metadata.

      Equations
      Instances For

        Like getAppNumArgs but ignores metadata.

        Instances For
          @[inline]
          def Lean.Expr.withApp' {α : Sort u_1} (e : Lean.Expr) (k : Lean.ExprArray Lean.Exprα) :
          α

          Like withApp but ignores metadata.

          Instances For
            @[specialize #[]]
            def Lean.Expr.withApp'.go {α : Sort u_1} (k : Lean.ExprArray Lean.Exprα) :
            Lean.ExprArray Lean.ExprNatα

            Auxiliary definition for withApp'.

            Equations
            Instances For
              @[inline]

              Like getAppArgs but ignores metadata.

              Instances For
                def Lean.Expr.traverseApp' {m : TypeType u_1} [Monad m] (f : Lean.Exprm Lean.Expr) (e : Lean.Expr) :

                Like traverseApp but ignores metadata.

                Instances For
                  @[inline]
                  def Lean.Expr.withAppRev' {α : Sort u_1} (e : Lean.Expr) (k : Lean.ExprArray Lean.Exprα) :
                  α

                  Like withAppRev but ignores metadata.

                  Instances For
                    @[specialize #[]]
                    def Lean.Expr.withAppRev'.go {α : Sort u_1} (k : Lean.ExprArray Lean.Exprα) :

                    Auxiliary definition for withAppRev'.

                    Equations
                    Instances For
                      @[inline]

                      Like getAppRevArgs but ignores metadata.

                      Instances For
                        @[inline]

                        Like getRevArg! but ignores metadata.

                        Equations
                        Instances For
                          @[inline]

                          Like getArgD but ignores metadata.

                          Instances For
                            @[inline]

                            Like getArg! but ignores metadata.

                            Instances For

                              Like isAppOf but ignores metadata.

                              Instances For