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

Even with Tobias's suggestion, I suspect you wouldn't get executable code since your labels are "parametrized":
```
>> consts max_label :: nat
>> typedef Label = "{n :: nat. n <= max_label }" by fastsimp

```
Here you "declare" max_label but not define it. It you were to program this by yourself in ML, you would need the value max_label either as a constant or as a parameter.
```
Amine.

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.
```
Tobias

Sven Schneider schrieb:
```
```Dear all,

```
I am not able to create code from the theory below. Unfortunately I can't understand the message (see bellow) that I get. I guess it has something todo with the part 1.5.3 in the manual of the codegeneration (Concerning operational equality).
```
All the best
Sven

*** No type arity Label :: eq,
*** for constant eval
*** in defining equations
*** "eval (Obj ?x) Â›Âº card (dom ?x)"
*** "eval (Var ?n) Â›Âº ?n",
*** while preprocessing equations for constant(s) eval
*** At command "export_code".

theory Gentest imports Main begin

consts max_label :: nat
typedef Label = "{n :: nat. n <= max_label }" by fastsimp

datatype dB =
Var "nat"
| Obj "Label \<Rightarrow> dB option"

constdefs compare :: "Label \<Rightarrow> Label \<Rightarrow> bool"
"compare k l \<equiv> (Rep_Label k = Rep_Label l)"

consts eval :: "dB \<Rightarrow> nat"
primrec
"eval (Var n) = n"
"eval (Obj x) = card (dom x)"

lemma "eval (Obj(empty(Abs_label (0::nat) \<mapsto>Var 2))) = ?x" by simp

export_code "eval" in "SML" file "gen.ML"
export_code "compare" in "SML" file "gen.ML"

end

```
```

```

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