[isabelle] Automatic derivation of a total order on datatypes



Hi,

is it possible to automa(t/g)ically instantiate a datatype as linorder,
if it is enough that there exists any order (e.g. the order of the
constructors in the definition with the restriction that all arguments
are of class linorder too)?

Use-case: Insert the datatype into a structure that needs an order on
its members. And if one does not care about the specific order, manually
defining it is quite cumbersome (especially for a large number of
constructors)...

Any hints on (semi-)automatic tools/tricks are highly appreciated :)

- René
-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.