[isabelle-dev] Frag / Poly_Mapping

[Akihisa Yamada]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>