English
A failsafe variant of decode; decode₂(α, n) returns the preimage of n under encode if it exists, otherwise none.
Русский
Функция decode₂ — запасной вариант decode; decode₂(α, n) возвращает предобраз n через encode, если он существует, иначе none.
LaTeX
$$$\\mathrm{decode}_2(\\alpha)(n) = \\mathrm{decode}(n)\\;\\text{bind}\\; (\\mathrm{Option}.guard\\; (\\lambda a. \\mathrm{encode}(a)=n)).$$$
Lean4
/-- Failsafe variant of `decode`. `decode₂ α n` returns the preimage of `n` under `encode` if it
exists, and returns `none` if it doesn't. This requirement could be imposed directly on `decode` but
is not to help make the definition easier to use. -/
def decode₂ (α) [Encodable α] (n : ℕ) : Option α :=
(decode n).bind (Option.guard fun a => encode a = n)
