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

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