English
Explicit decoding function for the sum α ⊕ β: decodeSum(n) yields a value in α ⊕ β by inspecting n and recursively decoding its components.
Русский
Явное декодирующее отображение для суммы α ⊕ β: decodeSum(n) получается путём анализа n и рекурсивного декодирования составляющих.
LaTeX
$$$ \mathrm{decodeSum}(n) = \begin{cases} (\mathrm{decode}(m)) \mapsto \mathrm{Sum.inl} & \text{if } \mathrm{boddDiv2}(n)=(\mathrm{false},m) \\ (\mathrm{decode}(m)) \mapsto \mathrm{Sum.inr} & \text{otherwise} \end{cases} $$$
Lean4
/-- Explicit decoding function for the sum of two encodable types. -/
def decodeSum (n : ℕ) : Option (α ⊕ β) :=
match boddDiv2 n with
| (false, m) => (decode m : Option α).map Sum.inl
| (_, m) => (decode m : Option β).map Sum.inr
