[isabelle] Binary tree exercise
I am a newbie. I was trying the binary tree exercise, and Isabelle is not
able to unify types. Here is my program.
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 "_
*** 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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and