Re: [isabelle] Nominal2 fails on Datatypes with Lists



Hi Wolfgang,

>So did I get this correctly that Nominal2 isn’t further developed
>anymore?

Yes, it is true that it is not currently on the top of my
to-do list. Sorry. I am also not aware whether anybody else
is tinkering with the code. It is part of the AFP and so
will be maintained and kept in a working state.

> By the way, is the restriction that values of a nominal data type may
> not contain functions also in place in Nominal2?

Yes, unless the function is "trivial" such as

nominal_datatype
      ty = TRecord "bool \<Rightarrow> char"
         | Test

Hope this helps,
Christian


________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Wolfgang Jeltsch <wolfgang-it at jeltsch.info>
Sent: 17 October 2019 16:31
To: cl-isabelle-users at lists.cam.ac.uk <cl-isabelle-users at lists.cam.ac.uk>
Subject: Re: [isabelle] Nominal2 fails on Datatypes with Lists

Hi, Christian!

So did I get this correctly that Nominal2 isn’t further developed
anymore?

By the way, is the restriction that values of a nominal data type may
not contain functions also in place in Nominal2?

All the best,
Wolfgang

Am Donnerstag, den 17.10.2019, 12:35 +0000 schrieb Urban, Christian:
> Hi Wolfgang,
>
>
> Is Nominal2 somehow production-ready?
>
> This depends on your point of view. ;o) It is certainly true that it
> quite rough and not all features are implemented. And it was aeons ago
> I have done things with it. But at the same time people have found it
> useful and have used it in interesting formalisations, for example
>
> https://eur03.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.isa-afp.org%2Fbrowser_info%2Fcurrent%2FAFP%2FIncompleteness%2F&amp;data=01%7C01%7Cchristian.urban%40kcl.ac.uk%7Cbac0eaf2865d405c566a08d75317466a%7C8370cf1416f34c16b83c724071654356%7C0&amp;sdata=s6JMWrL4auiYJIzYkyFs9HEwE6maeSio%2Bdp7OWMnTv8%3D&amp;reserved=0
>
> It really depends on what your point of view is and what you want to
> do.
>
> Christian
> ________________________________
> From: cl-isabelle-users-bounces at lists.cam.ac.uk <
> cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Wolfgang
> Jeltsch <wolfgang-it at jeltsch.info>
> Sent: 16 October 2019 22:04
> To: cl-isabelle-users at lists.cam.ac.uk <
> cl-isabelle-users at lists.cam.ac.uk>
> Subject: Re: [isabelle] Nominal2 fails on Datatypes with Lists
>
> Hi, Christian!
>
> Is Nominal2 somehow production-ready? From its website I got the
> impression that it had been developed only half-way and then
> development had halted.
>
> All the best,
> Wolfgang





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.