I am trying to use the export_code tool for the following definition:
definition set_to_list :: "('a×'a) set ⇒ ('a×'a) list"
where "set_to_list A = (SOME L. set L = A)"
This is not working due to missing code equations for Eps. Now I discovered that there is also a definition:
definition sorted_list_of_set :: "'a set ⇒ 'a list" where
"sorted_list_of_set = folding.F insort []"
However, I am not capable of asserting that ('a ×'a) is a linear order (which would be fine for me, e.g. first comparing the first element and then the second). Can someone help me to either fix my own definition or using the existing one?