[isabelle-dev] datatype takes minutes, but timing panel shows 10s
andreas.lochbihler at inf.ethz.ch
Tue Apr 14 09:14:29 CEST 2015
> the code plugin defines a new constant (copy of op =) that is used as equality.
> datatype x = A | B
> export_code equal_x_inst.equal_x in SML
This is precisely the instantiation of the equals type class.
> To get it executable (#constructors)^2 equations are proved in a backward fashion (I'm
> sure it could be easilly done in a forward fashion as well). However, this code goes back
> to Stefan and Florian, and we didn't attempt to optimize it when integrating it with the
> new package.
> But isn't the performance now (894d6d863823 ) already acceptable?
I have not tried it yet, because I am busy testing Isabelle2015-RC0.
More information about the isabelle-dev