Commit 2023-03-21 18:48 daef2b6c

View on Github →

feat(data/list/alist): recursion on alist using insert (#1724) Mathlib4 pair for https://github.com/leanprover-community/mathlib/pull/15434

Estimated changes

Modified Mathlib/Data/List/AList.lean

added def AList.insertRec

added theorem AList.insertRec_empty

added theorem AList.insertRec_insert

added theorem AList.insertRec_insert_mk

added theorem AList.insert_of_neg

added theorem AList.mk_cons_eq_insert

Modified Mathlib/Data/List/Sigma.lean

added theorem List.nodupKeys_of_nodupKeys_cons

added theorem List.not_mem_keys_of_nodupKeys_cons