English
The extract operation removes a key a from s and returns the corresponding value together with the remaining AList.
Русский
Операция extract удаляет ключ a из s и возвращает соответствующее значение вместе с оставшимся AList.
LaTeX
$$$ \mathrm{extract}(a, s) = \text{(Option}(\beta a) \times AList \beta) $$$
Lean4
/-- Erase a key from the map, and return the corresponding value, if found. -/
def extract (a : α) (s : AList β) : Option (β a) × AList β :=
have : (kextract a s.entries).2.NodupKeys := by rw [kextract_eq_dlookup_kerase]; exact s.nodupKeys.kerase _
match kextract a s.entries, this with
| (b, l), h => (b, ⟨l, h⟩)
