[isabelle-dev] Frag / Poly_Mapping

Manuel Eberl eberlm at in.tum.de
Mon Sep 24 18:49:47 CEST 2018

On 24/09/2018 18:41, Florian Haftmann wrote:
> First-letter abbreviations are not very self-explanatory though.  So I'd
> go with something more explicit like »finite_support_fun« – note that
> this type constructor does not show up in concrete type syntax, only in
> type class instantiations, so its length should be fine.

It does show up in the name of the operations you define on it and the
theorems you prove about it though.


-------------- next part --------------
A non-text attachment was scrubbed...
Name: pEpkey.asc
Type: application/pgp-keys
Size: 1757 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180924/fcd57a7d/attachment-0002.key>

More information about the isabelle-dev mailing list