Email Gateway (Aug 18 2022 at 18:22): Email Gateway (Aug 18 2022 at 18:22):From: Srinivasan Iyer <sviyer@cs.stanford.edu>
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
Email Gateway (Aug 18 2022 at 18:22):From: Tobias Nipkow <nipkow@in.tum.de>
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
Last updated: May 06 2024 at 20:16 UTC