# [isabelle] Primrec

Hi
I have a polymorphic datatype as follows
datatype 'a form:
ff
| 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
``as follows:
`
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
``written as
`
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?
`
Cheers
Peter

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*