Documentation

Mathlib.Logic.Function.FromTypes

Function types of a given heterogeneous arity #

This provides Function.FromTypes, such that FromTypes ![α, β] τ = α → β → τ. Note that it is often preferable to use ((i : Fin n) → p i) → τ in place of FromTypes p τ.

Main definitions #

def Function.FromTypes {n : } :
(Fin nType u)Type u → Type u

The type of n-ary functions p 0 → p 1 → ... → p (n - 1) → τ.

Equations
Instances For
    theorem Function.fromTypes_zero (p : Fin 0Type u) (τ : Type u) :
    theorem Function.fromTypes_cons {n : } (α : Type u) (p : Fin nType u) (τ : Type u) :
    @[simp]
    @[simp]
    def Function.fromTypes_zero_equiv (p : Fin 0Type u) (τ : Type u) :

    The definitional equality between 0-ary heterogeneous functions into τ and τ.

    Equations
    Instances For

      The definitional equality between ![]-ary heterogeneous functions into τ and τ.

      Equations
      Instances For
        @[simp]
        theorem Function.fromTypes_succ_equiv_apply {n : } (p : Fin (n + 1)Type u) (τ : Type u) (a : Function.FromTypes p τ) :
        @[simp]
        theorem Function.fromTypes_succ_equiv_symm_apply {n : } (p : Fin (n + 1)Type u) (τ : Type u) (a : Function.FromTypes p τ) :

        The definitional equality between p-ary heterogeneous functions into τ and function from vecHead p to (vecTail p)-ary heterogeneous functions into τ.

        Equations
        Instances For
          @[simp]
          theorem Function.fromTypes_cons_equiv_apply {n : } (α : Type u) (p : Fin nType u) (τ : Type u) (a : Function.FromTypes (Matrix.vecCons α p) τ) :
          @[simp]
          theorem Function.fromTypes_cons_equiv_symm_apply {n : } (α : Type u) (p : Fin nType u) (τ : Type u) (a : Function.FromTypes (Matrix.vecCons α p) τ) :
          (Function.fromTypes_cons_equiv α p τ).symm a = a
          def Function.fromTypes_cons_equiv {n : } (α : Type u) (p : Fin nType u) (τ : Type u) :

          The definitional equality between (vecCons α p)-ary heterogeneous functions into τ and function from α to p-ary heterogeneous functions into τ.

          Equations
          Instances For
            def Function.FromTypes.const {n : } (p : Fin nType u) {τ : Type u} (t : τ) :

            Constant n-ary function with value t.

            Equations
            Instances For
              @[simp]
              theorem Function.FromTypes.const_zero (p : Fin 0Type u) {τ : Type u} (t : τ) :
              @[simp]
              theorem Function.FromTypes.const_succ {n : } (p : Fin (n + 1)Type u) {τ : Type u} (t : τ) :
              theorem Function.FromTypes.const_succ_apply {n : } (p : Fin (n + 1)Type u) {τ : Type u} (t : τ) (x : p 0) :
              instance Function.FromTypes.inhabited {n : } {p : Fin nType u} {τ : Type u} [Inhabited τ] :
              Equations