Re: [isabelle] Nominal2 Errors in simple datatype declarations



Hi Christian,

That indeed works. However, this came up because originally I was trying to
declare something like
"
nominal_datatype A = A "(name * B) list"
and B = B nat
"

Which throws the same exception. I can get around this as well by defining
"A" similarly to a list, and indeed that's the solution used in
"Nominal/Ex/Lambda.thy:24", but I'd prefer to be able to use other
datatypes in my definitions (redefining "'a set", for instance, wouldn't be
quite as easy...).

On Thu, 4 Aug 2016 at 18:58 Urban, Christian <christian.urban at kcl.ac.uk>
wrote:

> This is because you declare A to have a pair-type. It should
>
> work if you say
>
>
>   ... = A name B
>
>
> and it should have the same effect, except that you do not
>
> write
>
>
>   A (x,b)
>
>
> but
>
>
>  A x b
>
>
> Hope this helps,
>
> Christian
>
>
> PS: I am on vacation until next week...if more problems crop up,
>
> I might not be very quick with responding, but I try to keep an
>
> eye on my email.
> ------------------------------
> *From:* Edward Pierzchalski <e.a.pierzchalski at gmail.com>
> *Sent:* 04 August 2016 09:28:23
> *To:* cl-isabelle-users at lists.cam.ac.uk; Urban, Christian
> *Subject:* Nominal2 Errors in simple datatype declarations
>
> Hi, I'm getting some mysterious issues using the Nominal2 package. In the
> following minimal example:
>
> "
> theory Test
> imports Main "Nominal/Nominal2"
> begin
>
> atom_decl name
>
> nominal_datatype A = A "(name * B)"
> and B = B nat
>
> end
> "
>
> I get an "UnequalLengths" exception raised by line 544 of "library.ML"
> which defines list zip ("~~"). Unfortunately, I don't know how to get stack
> traces out of Isabelle theory runs. Any ideas on what's going on?
>



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