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,
Dmitriy

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)

Andreas






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