Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem

Hello Tobias,

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 MHonArc.