Hi Dmitriy,
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.
I see.
But isn't the performance now (894d6d863823 ) already acceptable?
I have not tried it yet, because I am busy testing Isabelle2015-RC0.
Cheers,
Andreas
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
