English
Explicit decoding function for Sigma γ: decodeSigma(n) decodes n into a Sigma γ via unpairing n into (n1,n2) and decoding n1 and n2 accordingly.
Русский
Явное декодирующее отображение для Sigma γ: decodeSigma(n) декодирует n в Sigma γ через разбор n на (n1,n2) и соответствующее декодирование.
LaTeX
$$$ \mathrm{decodeSigma}(n) = \text{let }(n_1,n_2) = \mathrm{unpair}(n)\ \text{in} \ (\mathrm{decode}(n_1)) \bind \lambda a \; (\mathrm{decode}(n_2)).\text{map }(\lambda b. \Sigma\;\, a\, b)$$$
Lean4
/-- Explicit decoding function for `Sigma γ` -/
def decodeSigma (n : ℕ) : Option (Sigma γ) :=
let (n₁, n₂) := unpair n
(decode n₁).bind fun a => (decode n₂).map <| Sigma.mk a
