Re: [isabelle] Isabelle2014-RC1: defaults for (co)datatype selectors



Hi Andreas,

Am 29.07.2014 um 14:56 schrieb Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>:

> In Isabelle2013-2, one could declare a selector name that hides another constant.
> For example, in the following declaration, the new selector tl hides the constant "List.tl".
> 
> codatatype 'a llist = LNil (defaults tl: LNil) | LCons 'a (tl: "'a llist")
> 
> In Isabelle2014-RC1, defaults must be specified in a separate where clause, so I tried the following:
> 
> codatatype 'a llist = LNil | LCons 'a (tl: "'a llist") where "tl LNil = LNil"
> 
> However, this results in a type error, because tl in the where clause is parsed as List.tl. How can I use existing names for selectors with defaults in the new format?

Thank you for the report. Funnily enough, I had thought about the issue; there's some code in "ctr_sugar.ML" that created an appropriate context precisely to avoid the problem you just described. Unfortunately, despite all its good will, this code was executed only for the "free_constructors" command, not for "datatype_new" or "codatatype". This is solved by the attached change.

Makarius: Could you import the following change? (I have no idea if the CRLF quirk is still affecting my email client, but please do your usual magic.) The issue is a regression w.r.t. Isabelle2013-2, so it would be nice to have it fixed. Thanks.

Jasmin

Attachment: sel_default_lthy
Description: Binary data



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