Hi Matthieu,
I have written a little ML library allowing to automatically prove, in most
cases, instantiations of types (typedefs, records and datatypes) as countable
(see ~~/src/HOL/Library/Countable).
It seems that for datatypes we now have such functionality, implemented
four weeks ago by Brian Huffman:
http://isabelle.in.tum.de/repos/isabelle/rev/15df7bc8e93f
It comes in the form of a method, so it has to be invoked explicitly,
but like this it doesn't produce any penalty when it is not used. If you
want to contribute an extension to records/typedefs, you are welcome,
but you probably want to study Brian's implementation first. I assume
that he is also the most appropriate person to review patches for this
functionality.
Alex
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
