[isabelle-dev] sets and code generation

[Christian Sternagel]

Hi there,

since set is a proper type some code equations that used to work, no 
longer do, e.g.,

"op |> = {(x, y). supt_impl x y}"

as a code equation leads to an error stating that terms (x and y are 
first-order terms) do not support the enum class. Since the possible 
terms (using strings as function symbols and variables) cannot be 
enumerated in a (finite) list, I can also not introduce an enum instance.

In the NEWS I found that the default setup for sets during code 
generation is as a container type (instead of predicates). What are the 
reasons for this decision? Is there an easy fix for such code equations?

One other thing. Syntax (e.g., ord) suggests "'a => 'a => bool" for 
relations, but the library support (starting with more standard symbols) 
is leaning towards "'a rel". As a user it would be nice to have some 
indication what is preferable/best practice (e.g., in terms of future 
support; I already switched several times in our IsaFoR formalization, 
currently rewrite relations are of type "('f, 'v) term rel", is this the 
way to go?).

cheers

chris