Re: [isabelle] selector name in datatype_new causes proof failure

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,

On 02.09.2014 10:26, Andreas Lochbihler wrote:
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)


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