Theorems · Definition

AList.insert

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

Insert a key-value pair into an association list and erase any existing pair with the same key.

Defined in

Mathlib.Data.List.AList

Cited by

27 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

DecidableEq