Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem
Not being able to transform anything to code that involes sets or
functions seems to be a very strong restriction to me. Even though
"card (dom x)" is just an example and changing it to "0" solves the
'type arity'-Problem changing it does not solve my initial problem.
Is there a list of what can/can't be executed and what will/will not be
made executable in the near future? If it is in the manual I missed it.
I guess I have to thing about changing everything to lists or similar.
Thanks a lot and have a nice day!
On Tue, 20 Nov 2007, Tobias Nipkow wrote:
I'm not sure about the arity problem. But
"eval (Obj x) = card (dom x)"
is unlikely to be executable: dom is defined by set comprehension, which is
not executable, and the definition of card has similar problems.
If you need to compute dom and card, I suspect you need to replace functions
by a special data structure like an association list (see
Library/AssocList.thy) or even search trees.
This archive was generated by a fusion of
Pipermail (Mailman edition) and