Re: [isabelle] Using typedef_overloaded in future releases of Isabelle

You can say:

record (overloaded) 'i simple_foo =
  myString :: string
  myWord :: "'i::len word"


> On 04.05.2016, at 01:33, C. Diekmann <diekmann at> wrote:
> Dear list,
> I'm using a record which contains a machine word of arbitrary length.
> record 'i simple_foo = myString :: string
>                                   myWord :: "'i::len word"
> To make this work, I need to state the following:
>  declare[[typedef_overloaded]]
> Whenever I'm relying on `declare` or similar low-level magic, I'm afraid
> that things will break easily. Will this continue to work in upcoming
> releases? Is this the intended or official way to achieve what I want to do?
> Will the record package be made context-aware such that I don't need the
> global `declare`? I would like to write the following:
> context
>  notes [[typedef_overloaded]]
> begin
>  record 'i simple_foo = myString :: string
>                                     myWord :: "'i::len word"
> end
> Best Regards,
>  Cornelius


The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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