From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear BNF developers,
in Isabelle2014, the datatype_new declaration below results in a proof failure. If I
remove the selector name specification bar, the proof succeeds. Is there anything I can do
to get the selector names I want?
datatype_new ('t, 'id) foo =
Foo "('t list ⇒ 't) + 't"
| Bar (bar: 'id)
Andreas
From: Dmitriy Traytel <traytel@in.tum.de>
Hi Andreas,
if no selector is specified for datatypes, there will be none generated
(a recent policy change). Your example shows tactic failures in the case
when selectors are generated, so the problem is even worse than just
getting the right name. Fortunately, there is a simple workaround in
this case:
datatype_new (dead 't, 'id) foo =
Foo "('t list ⇒ 't) + 't"
| Bar (bar: 'id)
Marking 't explicitly as dead, changes the underlying BNFs slightly and
the tactic succeeds. In the repository version we will make the tactic
more robust also in the other case.
Thanks for the report,
Dmitriy
Last updated: Apr 18 2024 at 08:19 UTC