On 03/21/2012 05:05 PM, Lukas Bulwahn wrote:
On 03/21/2012 08:36 AM, Christian Sternagel wrote:
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.
Introducing 'a set as a type constructor now allows us to refine the set
operations to operations on lists (by Florian's way of data refinement
for code generation).
However, this now disallows the execution of "op |>" on the type "...
set". To execute this, you have to move this specification to predicates
('a => bool):
Define "op |> = (%(x, y). supt_impl x y)"
Lukas
Sorry I don't quite get it. op |> is already defined to be of type
"('f, 'v) term rel" (and used heavily as a set). So the above equation
would not be well-typed. Is your suggestion to change op |> into a
predicate?
cheers
chris
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
