Documentation

Mathlib.Data.Fin.Tuple.Curry

Currying and uncurrying of n-ary functions #

A function of n arguments can either be written as f a₁ a₂ ⋯ aₙ or f' ![a₁, a₂, ⋯, aₙ]. This file provides the currying and uncurrying operations that convert between the two, as n-ary generalizations of the binary curry and uncurry.

Main definitions #

def Function.FromTypes.uncurry {n : } {p : Fin nType u} {τ : Type u} (f : Function.FromTypes p τ) :
((i : Fin n) → p i)τ

Uncurry all the arguments of Function.FromTypes p τ to get a function from a tuple.

Note this can be used on raw functions if used.

Equations
  • x.uncurry = fun (x_1 : (i : Fin 0) → x_4 i) => x
  • x.uncurry = fun (args : (i : Fin (n + 1)) → x_4 i) => (x (args 0)).uncurry ((fun {x : Fin n} => args) ∘' Fin.succ)
Instances For
    def Function.FromTypes.curry {n : } {p : Fin nType u} {τ : Type u} :
    (((i : Fin n) → p i)τ)Function.FromTypes p τ

    Curry all the arguments of Function.FromTypes p τ to get a function from a tuple.

    Equations
    Instances For
      @[simp]
      theorem Function.FromTypes.uncurry_apply_cons {n : } {α : Type u} {p : Fin nType u} {τ : Type u} (f : Function.FromTypes (Matrix.vecCons α p) τ) (a : α) (args : (i : Fin n) → p i) :
      f.uncurry (Fin.cons a args) = (f a).uncurry args
      @[simp]
      theorem Function.FromTypes.uncurry_apply_succ {n : } {p : Fin (n + 1)Type u} {τ : Type u} (f : Function.FromTypes p τ) (args : (i : Fin (n + 1)) → p i) :
      f.uncurry args = (f (args 0)).uncurry (Fin.tail args)
      @[simp]
      theorem Function.FromTypes.curry_apply_cons {n : } {α : Type u} {p : Fin nType u} {τ : Type u} (f : ((i : Fin (n + 1)) → Matrix.vecCons α p i)τ) (a : α) :
      Function.FromTypes.curry f a = Function.FromTypes.curry ((fun {x : (i : Fin n) → Matrix.vecCons α p i.succ} => f) ∘' Fin.cons a)
      @[simp]
      theorem Function.FromTypes.curry_apply_succ {n : } {p : Fin (n + 1)Type u} {τ : Type u} (f : ((i : Fin (n + 1)) → p i)τ) (a : p 0) :
      @[simp]
      theorem Function.FromTypes.curry_uncurry {n : } {p : Fin nType u} {τ : Type u} (f : Function.FromTypes p τ) :
      @[simp]
      theorem Function.FromTypes.uncurry_curry {n : } {p : Fin nType u} {τ : Type u} (f : ((i : Fin n) → p i)τ) :
      @[simp]
      theorem Function.FromTypes.curryEquiv_apply {n : } {τ : Type u} (p : Fin nType u) :
      ∀ (a : ((i : Fin n) → p i)τ), (Function.FromTypes.curryEquiv p) a = Function.FromTypes.curry a
      @[simp]
      theorem Function.FromTypes.curryEquiv_symm_apply {n : } {τ : Type u} (p : Fin nType u) (f : Function.FromTypes p τ) :
      ∀ (a : (i : Fin n) → p i), (Function.FromTypes.curryEquiv p).symm f a = f.uncurry a
      def Function.FromTypes.curryEquiv {n : } {τ : Type u} (p : Fin nType u) :
      (((i : Fin n) → p i)τ) Function.FromTypes p τ

      Equiv.curry for p-ary heterogeneous functions.

      Equations
      Instances For
        theorem Function.FromTypes.curry_two_eq_curry {p : Fin 2Type u} {τ : Type u} (f : ((i : Fin 2) → p i)τ) :
        def Function.OfArity.uncurry {α : Type u} {β : Type u} {n : } (f : Function.OfArity α β n) :
        (Fin nα)β

        Uncurry all the arguments of Function.OfArity α n to get a function from a tuple.

        Note this can be used on raw functions if used.

        Equations
        Instances For
          def Function.OfArity.curry {α : Type u} {β : Type u} {n : } (f : (Fin nα)β) :

          Curry all the arguments of Function.OfArity α β n to get a function from a tuple.

          Equations
          Instances For
            @[simp]
            theorem Function.OfArity.curry_uncurry {α : Type u} {β : Type u} {n : } (f : Function.OfArity α β n) :
            @[simp]
            theorem Function.OfArity.uncurry_curry {α : Type u} {β : Type u} {n : } (f : (Fin nα)β) :
            @[simp]
            theorem Function.OfArity.curryEquiv_apply {α : Type u} {β : Type u} (n : ) :
            ∀ (a : (Fin nα)β), (Function.OfArity.curryEquiv n) a = Function.FromTypes.curry a
            @[simp]
            theorem Function.OfArity.curryEquiv_symm_apply {α : Type u} {β : Type u} (n : ) (f : Function.FromTypes (fun (a : Fin n) => α) β) :
            ∀ (a : Fin nα), (Function.OfArity.curryEquiv n).symm f a = f.uncurry a
            def Function.OfArity.curryEquiv {α : Type u} {β : Type u} (n : ) :
            ((Fin nα)β) Function.OfArity α β n

            Equiv.curry for n-ary functions.

            Equations
            Instances For
              theorem Function.OfArity.curry_two_eq_curry {α : Type u} {β : Type u} (f : (Fin 2α)β) :