Theorems · Theorem

AList.insertRec.eq_def

∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {C : AList β → Sort u_1} (H0 : C ∅)
  (IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (AList.insert a b l)) (x : AList β),
  AList.insertRec H0 IH x =
    match x with
    | { entries := [], nodupKeys := nodupKeys } => H0
    | { entries := c :: l, nodupKeys := h } =>
      ⋯.mpr (IH c.fst c.snd { entries := l, nodupKeys := ⋯ } ⋯ (AList.insertRec H0 IH { entries := l, nodupKeys := ⋯ }))

Defined in

Mathlib.Data.List.AList

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEq