vector

Mathlib.Computability.Primrec

URI: https://scilib.ai/kg/mathlib#Primcodable.vector

English

The type List.Vector α n is primitive codable.

Русский

Тип List.Vector α n примитивно-кодируем.

LaTeX

$$$\mathrm{Primcodable}(\mathrm{List.Vector}(\alpha,n))$$$

Lean4

instance vector {n} : Primcodable (List.Vector α n) :=
  subtype ((@Primrec.eq ℕ _).comp list_length (const _))

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru