Re: [isabelle] Unable to generate code for ?P = (%x. True)



Tobias Nipkow wrote:
> definition
>   some_elem :: "'a set => 'a"
>   "some_elem == (%S. SOME x. x : S)"
> 
> consts_code
>   "some_elem" ("hd")

I forgot to add that this is inconsistent from a logical point of view:
it allows you to derive (via the ML level) that "some_elem {1,2} ~=
some_elem {2,1}". So beware of what you are doing when implementing SOME
by hand.

Tobias





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