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.