Re: [isabelle] primrec_new error: extra vars on RHS, option return type works

Dear Gottfried,

This looks like a primrec_new bug in Isabelle2013-2 (it works with "the" development version, e.g., 761e40ce91bc). As a workaround, you can wrap x in some function such as id.

primrec_new get_hS_FAILS :: "hD => hD fset" where
  "get_hS_FAILS hEM    = {||}"
 |"get_hS_FAILS (hS x) = id x"


On 24/01/14 07:40, G B wrote:

I'm using `datatype_new` like this:

datatype_new hD = hEM | hS "hD fset"

I then get the `primrec_new` error, "Extra variables on the rhs", for this function:

primrec_new get_hS_FAILS :: "hD => hD fset" where
   "get_hS_FAILS hEM    = {||}"
  |"get_hS_FAILS (hS x) = x"

Fortunately, this function works for me, where I use `hD fset option` as the return type:

primrec_new opt_hS :: "hD => hD fset option" where
   "opt_hS hEM    = None"
  |"opt_hS (hS x) = Some x"

The end result is that I have to use three functions instead of the one.

Is there a simple fix for this? I attach the theory.


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