Email Gateway (Aug 19 2022 at 15:06): Email Gateway (Aug 19 2022 at 15:06):From: Andreas Lochbihler <andreas.lochbihler@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?
Best,
Andreas
Email Gateway (Aug 19 2022 at 15:07):From: Jasmin Christian Blanchette <jasmin.blanchette@gmail.com>
Hi Andreas,
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
sel_default_lthy
Email Gateway (Aug 19 2022 at 15:10):From: Makarius <makarius@sketis.net>
OK, see
https://bitbucket.org/isabelle_project/isabelle-release/commits/2d0f0d6fdf3
so it will be in the next release candidate (next week).
Makarius
Last updated: Apr 24 2024 at 20:16 UTC