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.

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

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

          Like withApp but ignores metadata.

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

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

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[inline]
                  def Lean.Expr.withAppRev' {α : Sort u_1} (e : Lean.Expr) (k : Lean.ExprArray Lean.Exprα) :
                  α

                  Like withAppRev but ignores metadata.

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

                      Equations
                      Instances For

                        Like getRevArgD but ignores metadata.

                        Equations
                        Instances For
                          @[inline]

                          Like getArgD but ignores metadata.

                          Equations
                          Instances For

                            Like isAppOf but ignores metadata.

                            Equations
                            Instances For

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

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

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

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