Re: [isabelle] Datatype: Sort constraint and nested datatypes
Coming back to an old thread:
> On 02.02.2016, at 15:14, Peter Lammich <lammich at in.tum.de> wrote:
> datatype 'a::order undef = Undefined | Defined "'a"
> datatype 'a::order node = Node "'a node undef"
> The second command raises:
> Tactic failed
> The error(s) above occurred for the goal statementâ:
> âf g. size_node f â map_node g = size_node (f â g)
> This does not occur if one removes the sort constraint on undef. The
> sort constraint on Node seems to be unrelated.
> This behaviour is present in Isabelle2015, and also in 2016-RC3.
> (Partial) workaround: The well-known Imperative-HOL hack gives you back
> some of the sort contraints:
Another workaround would be to pass (plugins del: size) right after the "datatype" keyword. Then you can define the size function manually.
In any case, I have just pushed a change to Testboard to address this. The change will likely not be part of the next release, but of Isabelle2017, since there are many workarounds.
This archive was generated by a fusion of
Pipermail (Mailman edition) and