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://www.isa-afp.org/browser_info/current/AFP/Incompleteness/
> 
> 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.