Re: [isabelle] Isabelle2016-RC0 - overloaded datatypes



Hi,

In Isabelle2015, I had the following datatype:

  datatype ('a::len0) wordinterval = WordInterval
                                        "('a::len0) word" --"start (inclusive)"
                                        "('a::len0) word" --"end (inclusive)"
                                  | RangeUnion "'a wordinterval" "'a
wordinterval"

With Isabelle2016-RC0, I get the following error:

Type definition with open dependencies, use "typedef (overloaded)" or
enable configuration option "typedef_overloaded" in the context.
  Type:  ('a, 'b) wordinterval_pre_wordinterval
  Deps:  len_of('a)
The error(s) above occurred in typedef
"wordinterval.wordinterval_pre_wordinterval"

The news describes this behavior for typedef. But how do I translate
my datatype to Isabelle2016?

Is typedef (overloaded) dangerous?

As an ordinary user, who does not dig into Isabelle internals too
much, trying to define a datatype and getting an error about typedef
is confusing.

Best Regards,
  Cornelius

2016-01-01 20:17 GMT+01:00 Makarius <makarius at sketis.net>:
> Dear Isabelle users,
>
> the coming Isabelle2016 release is scheduled for February 2016, after the
> next big Java 8 update by Oracle in January and some weeks before the
> deadline of ITP 2016.
>
> To get started with systematic testing there is now the relatively early
> http://isabelle.in.tum.de/website-Isabelle2016-RC0 (corresponding to
> Isabelle/e18444532fce and AFP/c62777f3e932).
>
> The website, NEWS, ANNOUNCE etc. are already mostly up-to-date.  Some
> documentation is still lagging behind, notably the Isabelle/jEdit manual.
> There are further fine points still to be sorted out.
>
>
> When discussing problems, observations, suggustions, etc. the mail subject
> line should be changed to something meaningful (but the release candidate
> number still given in the message body).
>
> As usual it is important to keep general laws of causality in mind: release
> candidates may still change, but the final release is final. Although this
> is tautological, in the past few releases we've often had complaints right
> after final lift-off, when it was too late.
>
> So the best time to start testing is now.
>
>
>         Makarius
>




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