[isabelle-dev] Frag / Poly_Mapping

[Lawrence Paulson]

It seems there is clearly a need for something of the sort to go into HOL/Library. Maybe it could be completely independent of Poly_Mapping, and the latter perhaps could be rewritten in terms of it.

Now who is volunteering to do this? I could certainly rewrite my "Frag.thy" to use the material I sent out yesterday and make independent of Poly_Mapping, but would that meet everyone's needs?

Larry

> On 25 Sep 2018, at 06:18, Akihisa Yamada <ayamada at trs.cm.is.nagoya-u.ac.jp> wrote:
> 
> 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