Documentation

Mathlib.Tactic.FunProp.ToBatteries

funProp missing function from standard library #

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

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

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

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

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

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