I have a polymorphic datatype as follows
datatype 'a form:
| Cpd 'a ('a form list)
I also have a function which, given a list of naturals, returns the
largest, called max_list. I want to define a function on my datatype
primrec depth :: 'a form => nat
depth ff = 0
depth Cpd f fs = max_list (map depth fs) + 1
Isabelle doesn't like it, giving me the error message
*** Entity to be defined occurs on rhs
*** The error(s) above occurred in definition "depth_form_def":
*** "depth =_ form_rec_1 (\ i. 0) (\ f fs fsa. max_list (map depth
fs) + 1) 0 undefined undefined"
*** At command "primrec".
(where =_ is the identity symbol, and \ is a lambda). Is this not a
proper recursive call? I think it should be. For instance, if it is
depth Cpd f [p,...q] = max_list [depth p,..., depth q]
then I think it is a recursive call. Can anyone point out how to fix
this, or why I am wrong in my belief?
This archive was generated by a fusion of
Pipermail (Mailman edition) and