Dear Alexander, Florian, Larry, Manuel,
recently I also made the same typedef, so that derivatives can be
defined, which wants real norm in current Isabelle/HOL. Unfortunately I
didn't notice it is called "poly_mapping".
I propose calling them finsupp or finite_supp. Support is often written
"supp", and the term in this meaning is clearly about functions so I
don't think "_fun" is needed.
Best regards,
Akihisa
On 2018/09/25 1:49, Manuel Eberl wrote:
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.
Manuel
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
