Documentation

Batteries.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
    @[inline]
    def Lean.Expr.withApp' {α : Sort u_1} (e : Expr) (k : ExprArray Exprα) :
    α

    Like withApp but ignores metadata.

    Equations
    Instances For
      @[specialize #[]]
      def Lean.Expr.withApp'.go {α : Sort u_1} (k : ExprArray Exprα) :
      ExprArray 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 : Exprm Expr) (e : 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 : Expr) (k : ExprArray Exprα) :
            α

            Like withAppRev but ignores metadata.

            Equations
            Instances For
              @[specialize #[]]
              def Lean.Expr.withAppRev'.go {α : Sort u_1} (k : ExprArray Exprα) :
              ExprArray 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]
                    def Lean.Expr.getArgD' (e : Expr) (i : Nat) (v₀ : Expr) (n : Nat := e.getAppNumArgs') :

                    Like getArgD but ignores metadata.

                    Equations
                    Instances For
                      def Lean.Expr.isAppOf' (e : Expr) (n : Name) :

                      Like isAppOf but ignores metadata.

                      Equations
                      Instances For

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

                        Equations
                        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