Re: [isabelle] Nominal2 Errors in simple datatype declarations



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

On Thursday, August 4, 2016 at 09:49:48 (+0000), Edward Pierzchalski wrote:
 >    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
 >    <[1]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 <[2]e.a.pierzchalski at gmail.com>
 >    Sent: 04 August 2016 09:28:23
 >    To: [3]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?
 > 
 > References
 > 
 >    1. mailto:christian.urban at kcl.ac.uk
 >    2. mailto:e.a.pierzchalski at gmail.com
 >    3. mailto:cl-isabelle-users at lists.cam.ac.uk

-- 




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