OfArity — Mathlib

English

The type OfArity(α, β, n) represents the type of n-ary functions α → α → ... → β.

Русский

Тип OfArity(α,β,n) представляет собой множество n-арных функций α → α → ... → β.

LaTeX

$$$$\mathrm{OfArity}(\alpha,\beta,n) = \mathrm{FromTypes} (\lambda _ : \mathrm{Fin}(n), \alpha) \beta.$$$$

Lean4

/-- 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 β`. -/
abbrev OfArity (α β : Type u) (n : ℕ) : Type u :=
  FromTypes (fun (_ : Fin n) => α) β

Похожие утверждения