# Re: [isabelle] Binary tree exercise

Remember that in functional programming "f a b c d" means that f is a
function of 4 arguments. You want "inorder (Node xs ys zs)".
Tobias
Am 11/09/2011 07:56, schrieb Srinivasan Iyer:
> 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.*