Re: [isabelle] Automatic derivation of a total order on datatypes
The derive linorder works really well, but I've come across an odd example
which doesn't work, namely:
datatype vbasic = BoolI bool | ListI "vbasic list"
derive linorder vbasic
Fails to prove. If I replace the bool with an int or remove the list
constructor, it works fine. There seems to be an odd interaction between
bool and list. The following works fine:
datatype vbasic = TrueI | FalseI | IntI "int" | ListI "vbasic list"
Do you know what's causing this?
On 14 November 2012 09:42, René Thiemann <rene.thiemann at uibk.ac.at> wrote:
> Dear René
> as Andreas already stated, there is such an order generator in the AFP.
> However, the tactics in the AFP-Entry for the Isabelle2012 release version
> contain some known gaps, so that the generator may fail on some datatypes.
> All known gaps have been fixed in the development version of the AFP.
> So, if you are working with the development version of Isabelle, just use
> the development version of the AFP.
> If however, you are working with Isabelle2012, then please download a
> fixed version of the AFP-entry at
> which contains all the fixes of the order generator and works with
> Best regards,
This archive was generated by a fusion of
Pipermail (Mailman edition) and