[isabelle] primrec of datatype containing fset



Iâd like to write recursive functions over the following datatype:

datatype val = VNat nat | VRel "(val à val) fset"

As a simple example,

primrec count :: "val â nat" where
  "count (VNat n) = 1" |
  "count (VRel t) = (ffold (Î (v1,v2). Î r. count v1 + count v2 + r) 0 t)"

But this getâs rejected with the âInvalid map functionâ error.

Whatâs the correct way to do this?

Cheers,
Jeremy

__________________________________________
Jeremy G. Siek    <jsiek at indiana.edu<mailto:jsiek at indiana.edu>>
Associate Professor
School of Informatics and Computing
Indiana University Bloomington
http://homes.soic.indiana.edu/jsiek/





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