Email Gateway (Jun 14 2026 at 10:43): Email Gateway (Jun 14 2026 at 10:43):From: Lawrence Paulson <lp15@cam.ac.uk>
I'm happy to welcome a contribution that takes a different tack from our recent flood of mathematical results. We haven't had anything about codatatypes in a long time.
Formalization of Countable Multisets
Mathias Schack Rabing and Dmitriy Traytel
Abstract
We define countable multisets as a generalization of finite multisets. Countable multisets are equivalently represented as functions from elements to extended natural numbers () returning non-zero values for countably many elements, or as quotients of lazy lists modulo infinitary permutations. We register countable multisets as a bounded natural functor (BNF), enabling nested (co)recursion through them in (co)datatypes. We further define the subtype of countably infinite multisets and register it as a BNF, too.
https://isa-afp.org/entries/Countable_Multiset.html
Last updated: Jul 02 2026 at 07:34 UTC