English
The decoding of a product using the encodable structure is given by decoding the first component and then decoding the second, pairing the results.
Русский
Декодирование произведения через кодируемую структуру задаётся как: сначала декодируем первый компонент, затем второй, затем собираем кортеж.
LaTeX
$$$ \mathrm{decode}_{\alpha \times \beta}(n) = (\mathrm{decode}(n.1)).bind \lambda a. (\mathrm{decode}(n.2)).map (\lambda b. (a,b))$$$
Lean4
@[simp]
theorem decode_prod_val (n : ℕ) :
(@decode (α × β) _ n : Option (α × β)) = (decode n.unpair.1).bind fun a => (decode n.unpair.2).map <| Prod.mk a :=
by
simp only [decode_ofEquiv, Equiv.symm_symm, decode_sigma_val]
cases (decode n.unpair.1 : Option α) <;> cases (decode n.unpair.2 : Option β) <;> rfl
