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



You can say:

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

Cheers,
Gerwin



> On 04.05.2016, at 01:33, C. Diekmann <diekmann at in.tum.de> 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.