nil

Mathlib.Computability.Halting

URI: https://scilib.ai/kg/mathlib#Nat.Partrec'.nil

English

The constant empty vector is Partrec' (the vector-valued function that returns nil).

Русский

Постоянная пустая векторная функция является Partrec'.

LaTeX

$$$$\forall n,\; \mathrm{Nat.Partrec'.Vec}(\text{fun } x \mapsto \text{List.Vector.nil}).$$$$

Lean4

protected theorem nil {n} : @Vec n 0 fun _ => nil := fun i => i.elim0

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

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

Разделы

Аффилиация

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