[isabelle] Using typedef_overloaded in future releases of Isabelle



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



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