dedupKeys

Mathlib.Data.List.Sigma

URI: https://scilib.ai/kg/mathlib#List.dedupKeys

Lean4

/-- Remove entries with duplicate keys from `l : List (Sigma β)`. -/
def dedupKeys : List (Sigma β) → List (Sigma β) :=
  List.foldr (fun x => kinsert x.1 x.2) []

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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