Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Using typedef_overloaded in future releases of...


view this post on Zulip Email Gateway (Aug 22 2022 at 13:15):

From: "C. Diekmann" <diekmann@in.tum.de>
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

view this post on Zulip Email Gateway (Aug 22 2022 at 13:16):

From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
You can say:

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

Cheers,
Gerwin


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.


Last updated: Mar 28 2024 at 20:16 UTC