Theorems · Definition

List.kinsert

{α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → β a → List (Sigma β) → List (Sigma β)

Insert the pair ⟨a, b⟩ and erase the first pair with the key a.

Defined in

Mathlib.Data.List.Sigma

Cited by

9 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms

Assumes

DecidableEq