Fri, 14 Feb 2014 16:22:09 +0100 | blanchet | added examples/tests | changeset | files |
Fri, 14 Feb 2014 16:21:41 +0100 | blanchet | tuned code to allow mutualized corecursion through different functions with the same target type | changeset | files |
Fri, 14 Feb 2014 15:39:43 +0100 | blanchet | removed assumption in 'primrec_new' that a given constructor can only occur once | changeset | files |
Fri, 14 Feb 2014 15:14:35 +0100 | blanchet | generate unique names | changeset | files |
Fri, 14 Feb 2014 15:03:24 +0100 | blanchet | allow different functions to recurse on the same type, like in the old package | changeset | files |
Fri, 14 Feb 2014 15:03:23 +0100 | blanchet | improved 'datatype_new_compat': generate more fixpoint equations for types like 'datatype_new x = C (x list) (x list)' (here, one equation for each x list instead of a single for both), for higher compatibility + code generation attributes on the recursor | changeset | files |