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 #

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

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

Equations
Instances For
    source
    theorem Function.fromTypes_zero (p : Fin 0 → Type u) (τ : Type u) :
    Function.FromTypes p τ = τ
    source
    theorem Function.fromTypes_nil (τ : Type u) :
    Function.FromTypes ![] τ = τ
    source
    theorem Function.fromTypes_succ {n : ℕ} (p : Fin (n + 1) → Type u) (τ : Type u) :
    Function.FromTypes p τ = (Matrix.vecHead p → Function.FromTypes (Matrix.vecTail p) τ)
    source
    theorem Function.fromTypes_cons {n : ℕ} (α : Type u) (p : Fin n → Type u) (τ : Type u) :
    Function.FromTypes (Matrix.vecCons α p) τ = (α → Function.FromTypes p τ)
    source
    def Function.fromTypes_zero_equiv (p : Fin 0 → Type u) (τ : Type u) :
    Function.FromTypes p τ ≃ τ

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

    Equations
    Instances For
      source
      @[simp]
      theorem Function.fromTypes_zero_equiv_symm_apply (p : Fin 0 → Type u) (τ : Type u) (a : Function.FromTypes p τ) :
      (Function.fromTypes_zero_equiv p τ).symm a = a
      source
      @[simp]
      theorem Function.fromTypes_zero_equiv_apply (p : Fin 0 → Type u) (τ : Type u) (a : Function.FromTypes p τ) :
      (Function.fromTypes_zero_equiv p τ) a = a
      source
      def Function.fromTypes_nil_equiv (τ : Type u) :
      Function.FromTypes ![] τ ≃ τ

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

      Equations
      Instances For
        source
        @[simp]
        theorem Function.fromTypes_nil_equiv_symm_apply (τ : Type u) (a : Function.FromTypes ![] τ) :
        (Function.fromTypes_nil_equiv τ).symm a = a
        source
        @[simp]
        theorem Function.fromTypes_nil_equiv_apply (τ : Type u) (a : Function.FromTypes ![] τ) :
        (Function.fromTypes_nil_equiv τ) a = a
        source
        def Function.fromTypes_succ_equiv {n : ℕ} (p : Fin (n + 1) → Type u) (τ : Type u) :
        Function.FromTypes p τ ≃ (Matrix.vecHead p → Function.FromTypes (Matrix.vecTail 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
          source
          @[simp]
          theorem Function.fromTypes_succ_equiv_apply {n : ℕ} (p : Fin (n + 1) → Type u) (τ : Type u) (a : Function.FromTypes p τ) :
          (Function.fromTypes_succ_equiv p τ) a = a
          source
          @[simp]
          theorem Function.fromTypes_succ_equiv_symm_apply {n : ℕ} (p : Fin (n + 1) → Type u) (τ : Type u) (a : Function.FromTypes p τ) :
          (Function.fromTypes_succ_equiv p τ).symm a = a
          source
          def Function.fromTypes_cons_equiv {n : ℕ} (α : Type u) (p : Fin n → Type u) (τ : Type u) :
          Function.FromTypes (Matrix.vecCons α p) τ ≃ (α → Function.FromTypes p τ)

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

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

            Constant n-ary function with value t.

            Equations
            Instances For
              source
              @[simp]
              theorem Function.FromTypes.const_zero (p : Fin 0 → Type u) {τ : Type u} (t : τ) :
              Function.FromTypes.const p t = t
              source
              @[simp]
              theorem Function.FromTypes.const_succ {n : ℕ} (p : Fin (n + 1) → Type u) {τ : Type u} (t : τ) :
              Function.FromTypes.const p t = fun (x : Matrix.vecHead p) => Function.FromTypes.const (Matrix.vecTail p) t
              source
              theorem Function.FromTypes.const_succ_apply {n : ℕ} (p : Fin (n + 1) → Type u) {τ : Type u} (t : τ) (x : p 0) :
              Function.FromTypes.const p t x = Function.FromTypes.const (Matrix.vecTail p) t
              source
              instance Function.FromTypes.inhabited {n : ℕ} {p : Fin n → Type u} {τ : Type u} [Inhabited τ] :
              Inhabited (Function.FromTypes p τ)
              Equations