encode_list_cons

Mathlib.Logic.Equiv.List

URI: https://scilib.ai/kg/mathlib#Encodable.encode_list_cons

English

Encoding of a cons cell a :: l equals succ (pair (encode a) (encode l)).

Русский

Кодирование списка a :: l равно succ (pair (encode a) (encode l)).

LaTeX

$$$\\encode( a :: l ) = \\operatorname{succ}( \\operatorname{pair}( \\encode a)(\\encode l) )$$$

Lean4

@[simp]
theorem encode_list_cons (a : α) (l : List α) : encode (a :: l) = succ (pair (encode a) (encode l)) :=
  rfl

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

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

Разделы

Аффилиация

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