init

Mathlib.Tactic.MkIffOfInductiveProp

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.MkIff.List.init

Lean4

/-- Drops the final element of a list. -/
def init {α : Type*} : List α → List α
  | [] => []
  | [_] => []
  | a :: l => a :: init l

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

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

Разделы

Аффилиация

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