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