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
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: Apr 29 2024 at 12:29 UTC