Discussion:
[isabelle] Nominal2 Errors in simple datatype declarations
(too old to reply)
Urban, Christian
2016-08-04 09:01:25 UTC
Permalink
Raw Message
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 <***@gmail.com>
Sent: 04 August 2016 09:28:23
To: cl-isabelle-***@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?
Christian Urban
2016-08-05 08:44:51 UTC
Permalink
Raw Message
Hi Edward,

Yes, unfortunately things like

nominal_datatype A = A "(name * B) list"

do not work with nominal_datatype and you would have to
implement such terms with your own "copy" of lists.

Best wishes,
Christian
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
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.
__________________________________________________________________
Sent: 04 August 2016 09:28:23
Subject: Nominal2 Errors in simple datatype declarations
Hi, I'm getting some mysterious issues using the Nominal2 package. In
"
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?
References
--
Edward Pierzchalski
2016-08-05 09:40:09 UTC
Permalink
Raw Message
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...).
Post by Urban, Christian
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.
------------------------------
*Sent:* 04 August 2016 09:28:23
*Subject:* Nominal2 Errors in simple datatype declarations
Hi, I'm getting some mysterious issues using the Nominal2 package. In the
"
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?
Loading...