*To*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Subject*: Re: [isabelle] primrec_new error: extra vars on RHS, option return type works*From*: G B <igbi at gmx.com>*Date*: Fri, 24 Jan 2014 10:44:37 -0600*Cc*: "cl-isabelle-users at lists.cam.ac.uk List" <cl-isabelle-users at lists.cam.ac.uk>, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*In-reply-to*: <8305217A-421B-4172-A6E5-23ECA015DDCD@gmail.com>*References*: <52E20AC4.1070101@gmx.com> <52E22C97.1070505@inf.ethz.ch> <8305217A-421B-4172-A6E5-23ECA015DDCD@gmail.com>*User-agent*: Mozilla/5.0 (Windows NT 6.1; WOW64; rv:11.0) Gecko/20120312 Thunderbird/11.0

[by Andreas]...As a workaround, you can wrap x in some function such as id.

Andreas, thanks again.

Incidentally, I'm wondering whether you really need the "hEM" constructor in datatype_new hD = hEM | hS "hD fset" The canonical definition of hereditarily finite sets reads datatype_new hD = hS "hD fset"

Jasmin,

So, I have to take a huge, time-consuming tangent on logic.

Regards, GB

**References**:**[isabelle] primrec_new error: extra vars on RHS, option return type works***From:*G B

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

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

- Previous by Date: Re: [isabelle] primrec_new error: extra vars on RHS, option return type works
- Next by Date: [isabelle] question
- Previous by Thread: Re: [isabelle] primrec_new error: extra vars on RHS, option return type works
- Next by Thread: [isabelle] question
- Cl-isabelle-users January 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list