Documentation

Mathlib.Tactic.FunProp.ToBatteries

funProp missing function from standard library #

Check if a can be obtained by removing elements from b.

Equations
    Instances For
      def Mathlib.Meta.FunProp.letTelescope {α : Type} {n : TypeType u_1} [MonadControlT Lean.MetaM n] [Monad n] (e : Lean.Expr) (k : Array Lean.ExprLean.Exprn α) :
      n α

      Telescope consuming only let bindings

      Equations
        Instances For
          def Lean.Expr.swapBVars (e : Expr) (i j : Nat) :

          Swaps bvars indices i and j

          NOTE: the indices i and j do not correspond to the n in bvar n. Rather they behave like indices in Expr.lowerLooseBVars, Expr.liftLooseBVars, etc.

          TODO: This has to have a better implementation, but I'm still beyond confused with how bvar indices work

          Equations
            Instances For

              For #[x₁, .., xₙ] create (x₁, .., xₙ).

              Equations
                Instances For

                  For (x₀, .., xₙ₋₁) return xᵢ but as a product projection.

                  We need to know the total size of the product to be considered.

                  For example for xyz : X × Y × Z

                  Equations
                    Instances For

                      For an element of a product type(of sizen) xs create an array of all possible projections i.e. #[xs.1, xs.2.1, xs.2.2.1, ..., xs.2..2]

                      Equations
                        Instances For

                          Uncurry function f in n arguments.

                          Equations
                            Instances For

                              Eta expand f in only one variable and reduce in others.

                              Examples:

                                f                ==> fun x => f x
                                fun x y => f x y ==> fun x => f x
                                HAdd.hAdd y      ==> fun x => HAdd.hAdd y x
                                HAdd.hAdd        ==> fun x => HAdd.hAdd x
                              
                              Equations
                                Instances For

                                  Apply the given arguments to f, beta-reducing if f is a lambda expression. This variant does beta-reduction through let bindings without inlining them.

                                  Example

                                  beta' (fun x => let y := x * x; fun z => x + y + z) #[a,b]
                                  ==>
                                  let y := a * a; a + y + b
                                  
                                  Equations
                                    Instances For

                                      Beta reduces head of an expression, (fun x => e) a ==> e[x/a]. This version applies arguments through let bindings without inlining them.

                                      Example

                                      headBeta' ((fun x => let y := x * x; fun z => x + y + z) a b)
                                      ==>
                                      let y := a * a; a + y + b
                                      
                                      Equations
                                        Instances For