English
There is an explicit decoding function for Multiset; decoding a number n yields the multiset obtained by decoding a list of α and then mapping via Multiset.ofList.
Русский
Существует явное декодирование мультимножества; декодирование числа n дает множество, получаемое из списка α с помощью Multiset.ofList.
LaTeX
$$$\\operatorname{decodeMultiset}(n) = \\operatorname{Option.map} \\bigl( \\operatorname{Multiset.ofList} \\bigr)\\bigl( \\operatorname{List.encodable.decode} n \\bigr).$$$
Lean4
/-- Explicit decoding function for `Multiset α` -/
def decodeMultiset (n : ℕ) : Option (Multiset α) :=
((↑) : List α → Multiset α) <$> decode (α := List α) n
