English
A function from the symmetric product of Option α that splits on whether none is present: it either separates a none or maps attached options to explicit values.
Русский
Функция кодирования из симметрического произведения над Option α, разветвляющаяся в зависимости от наличия none.
LaTeX
$$$\\mathrm{encode} : \\mathrm{Sym}(\\mathrm{Option}(\\alpha))\\ n.succ \\to \\mathrm{Sym}(\\mathrm{Option}(\\alpha))n \\oplus \\mathrm{Sym}(\\alpha) n.succ$$$
Lean4
/-- Function from the symmetric product over `Option` splitting on whether or not
it contains a `none`. -/
def encode [DecidableEq α] (s : Sym (Option α) n.succ) : Sym (Option α) n ⊕ Sym α n.succ :=
if h : none ∈ s then Sum.inl (s.erase none h)
else Sum.inr (s.attach.map fun o => o.1.get <| Option.ne_none_iff_isSome.1 <| ne_of_mem_of_not_mem o.2 h)
