[isabelle] Binary tree exercise



Hi,

I am a newbie. I was trying the binary tree exercise, and Isabelle is not
able to unify types. Here is my program.

theory tree
 imports Main
begin

datatype 'a btree = Tip | Node "'a btree" "'a" "'a btree"

primrec inorder :: "'a btree \<Rightarrow> 'a list" where
"inorder Tip = Nil" |
"inorder Node xs ys zs = Nil"

the error is :

*** Type unification failed: Clash of types "(_ \<Rightarrow> _)" and "_
tree.btree"
***
*** Type error in application: incompatible operand type
***
*** Operator:  (inorder\<Colon>('a tree.btree \<Rightarrow> 'a List.list))
:: ('a tree.btree \<Rightarrow> 'a List.list)
*** Operand:   tree.btree.Node :: (??'a tree.btree \<Rightarrow> (??'a
\<Rightarrow> (??'a tree.btree \<Rightarrow> ??'a tree.btree)))
***
*** At command "primrec" (line 7 of "/Users/sviyer/tree.thy")


Thanks for reading,
Srini




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