English
An explicit decoding function for lists is defined by recursively inverting the encoding using unpair and bounds on the second component, producing an option of a list.
Русский
Явное декодирование списка определяется рекурсивно через разворот кодировки с использованием unpair и ограничений на вторую компоненту, возвращая опцию списка.
LaTeX
$$$\\decodeList : \\mathbb{N} \\to \\text{Option}(\\text{List } \\alpha), \\; \\decodeList(0) = \\text{some } [] , \\; \\decodeList(\\text{succ } v) = \\text{...}$$$
Lean4
/-- Explicit decoding function for `List α` -/
def decodeList : ℕ → Option (List α)
| 0 => some []
| succ v =>
match unpair v, unpair_right_le v with
| (v₁, v₂), h =>
have : v₂ < succ v := lt_succ_of_le h
(· :: ·) <$> decode (α := α) v₁ <*> decodeList v₂
