instTraversableFlipNat — Mathlib

English

For a fixed length n, the functor sending a type X to the length-n vectors over X, with its type arguments flipped, is traversable. Its traverse and map operations are inherited from the standard Vector constructions.

Русский

Для фиксированной длины n функтор X ↦ Vector X n, после перестановки аргументов, является traversable. Операции обхода и отображения задаются стандартно через векторные конструкторы.

LaTeX

$$$\\mathrm{Traversable}(\\mathrm{flip}\\,\\mathrm{Vector}\\, n)$$$

Lean4

instance : Traversable.{u} (flip Vector n)
    where
  traverse := @Vector.traverse n
  map {α β} := @Vector.map.{u, u} α β n

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