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)".
Am 11/09/2011 07:56, schrieb Srinivasan Iyer:
> 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
> 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