Documentation

Mathlib.Logic.Function.OfArity

Function types of a given arity #

This provides Function.OfArity, such that OfArity α β 2 = α → α → β. Note that it is often preferable to use (Fin n → α) → β in place of OfArity n α β.

Main definitions #

source
@[reducible, inline]
abbrev Function.OfArity (α β : Type u) (n : ℕ) :
Type u

The type of n-ary functions α → α → ... → β.

Note that this is not universe polymorphic, as this would require that when n=0 we produce either Unit → β or ULift β.

Equations
Instances For
    source
    @[simp]
    theorem Function.ofArity_zero (α β : Type u) :
    OfArity α β 0 = β
    source
    @[simp]
    theorem Function.ofArity_succ (α β : Type u) (n : ℕ) :
    OfArity α β n.succ = (α → OfArity α β n)
    source
    def Function.OfArity.const (α : Type u) {β : Type u} (b : β) (n : ℕ) :
    OfArity α β n

    Constant n-ary function with value b.

    Equations
    Instances For
      source
      @[simp]
      theorem Function.OfArity.const_zero (α : Type u) {β : Type u} (b : β) :
      const α b 0 = b
      source
      @[simp]
      theorem Function.OfArity.const_succ (α : Type u) {β : Type u} (b : β) (n : ℕ) :
      const α b n.succ = fun (x : Matrix.vecHead fun (x : Fin n.succ) => α) => const α b n
      source
      theorem Function.OfArity.const_succ_apply (α : Type u) {β : Type u} (b : β) (n : ℕ) (x : α) :
      const α b n.succ x = const α b n
      source
      instance Function.OfArity.inhabited {α β : Type u_1} {n : ℕ} [Inhabited β] :
      Inhabited (OfArity α β n)
      Equations
      source
      theorem Function.FromTypes.fromTypes_fin_const (α β : Type u) (n : ℕ) :
      FromTypes (fun (x : Fin n) => α) β = OfArity α β n
      source
      def Function.FromTypes.fromTypes_fin_const_equiv (α β : Type u) (n : ℕ) :
      FromTypes (fun (x : Fin n) => α) β ≃ OfArity α β n

      The definitional equality between heterogeneous functions with constant domain and n-ary functions with that domain.

      Equations
      Instances For