[isabelle-dev] New lemmas about count_list

Martin Desharnais martin.desharnais at posteo.de
Fri Mar 4 09:38:06 CET 2022


Dear Tobias,

thanks for looking into it.

> Thus I would rather not create a growing count_list library, if it can 
> be avoided. Could you try to use the above hint and go via multisets? (I 
> may add one or two of your lemmas anyway, as a compromise)

I will try to replace all my usages of count_list by "count ∘ mset" and 
see how things turn out.

Cheers,
Martin
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_0x58AE985FE188789A.asc
Type: application/pgp-keys
Size: 3139 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220304/641a7b26/attachment.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 840 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20220304/641a7b26/attachment.sig>


More information about the isabelle-dev mailing list