English
For every key a and list l, kextract a l equals the pair (dlookup a l, kerase a l).
Русский
Для каждого ключа a и списка l функция kextract выдаёт пару (dlookup a l, kerase a l).
LaTeX
$$$kextract\\ a\\ l = (dlookup\\ a\\ l, kerase\\ a\\ l)$$$
Lean4
/-- Finds the first entry with a given key `a` and returns its value (as an `Option` because there
might be no entry with key `a`) alongside with the rest of the entries. -/
def kextract (a : α) : List (Sigma β) → Option (β a) × List (Sigma β)
| [] => (none, [])
| s :: l =>
if h : s.1 = a then (some (Eq.recOn h s.2), l)
else
let (b', l') := kextract a l
(b', s :: l')
