Email Gateway (Aug 22 2022 at 13:55): Email Gateway (Aug 22 2022 at 13:55):From: "Urban, Christian" <christian.urban@kcl.ac.uk>
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.
Email Gateway (Aug 22 2022 at 13:56):From: Christian Urban <christian.urban@kcl.ac.uk>
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
Email Gateway (Aug 22 2022 at 13:56):From: Edward Pierzchalski <e.a.pierzchalski@gmail.com>
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?
Email Gateway (Aug 22 2022 at 13:56):From: Edward Pierzchalski <e.a.pierzchalski@gmail.com>
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...).
Last updated: Apr 24 2024 at 01:07 UTC