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



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?

Best,
Andreas




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