Theorems · Theorem

AList.mk_cons_eq_insert

∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (c : Sigma β) (l : List (Sigma β)) (h : (c :: l).NodupKeys),
  { entries := c :: l, nodupKeys := h } = AList.insert c.fst c.snd { entries := l, nodupKeys := ⋯ }

Defined in

Mathlib.Data.List.AList

Cited by

1 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEq