[isabelle-dev] Frag / Poly_Mapping
ayamada at trs.cm.is.nagoya-u.ac.jp
Tue Sep 25 07:18:48 CEST 2018
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.
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.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev