English
extract(a,s) returns a pair (v, t) where v is the optional value at a in s, and t is s with a removed; i.e., erase a from s yields t and v records the value if present.
Русский
extract(a,s) возвращает пару (v,t), где v — опциональное значение по ключу a в s, а t — s без ключа a; то есть erase a s даёт t и v фиксирует значение при наличии.
LaTeX
$$$ extract\ (a:\alpha)\ (s:\ Finmap\, \beta) :\mathrm{Option}(\beta\ a) \times Finmap\, \beta = (v,t)\ \text{где}\ t = erase(a,s) \text{и } v \in \mathrm{Option}(\beta\ a) $$$
Lean4
/-- Erase a key from the map, and return the corresponding value, if found. -/
def extract (a : α) (s : Finmap β) : Option (β a) × Finmap β :=
(liftOn s fun t => Prod.map id AList.toFinmap (AList.extract a t)) fun s₁ s₂ p => by
simp [perm_lookup p, toFinmap_eq, perm_erase p]
