Re: [isabelle] Nominal2 Errors in simple datatype declarations



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.