Re: [isabelle] Isabelle2016-RC1: typedef-overloaded and records



Hi RenÃ,

The following does work

declare [[typedef_overloaded]]

record â

declare [[typedef_overloaded = false]]

But eventually the record package will be localized, and we wonât need such imperative declarations.

Dmitriy

> On 18 Jan 2016, at 12:51, Thiemann, Rene <Rene.Thiemann at uibk.ac.at> wrote:
> 
> Dear all,
> 
> when adapting our theories to Isabelle2016-RC1, I encountered a problem with the new upgrade of typedef and the overloaded constants.
> 
> Note that ('a,'b)rbt in "~~/src/HOL/Library/RBT" is such an overloaded type. As a user of RBTâs I now have to put a context around 
> other types that use RBTâs with a parametric 'a as in the example type âuse_rbt_Aâ.
> 
> However, the problem is that, I now cannot put these types into records or use records with generic RBTâs as arguments, since
> records are not localized. So, the creation of both types use_rbt_B and use_rbt_C fails.
> 
> Is there any known work-around to this problem? 
> (Except for converting the records into datatypes and then recursively wrap a context with [[typedef_overloaded]] around every further
> type declaration that transitively depends on these types)
> 
> With best regards,
> RenÃ
> 
> 
> theory Test
> imports
>  "~~/src/HOL/Library/RBT"
> begin
> 
> context
>  notes [[typedef_overloaded]]
> begin
> datatype 'a use_rbt_A = Foo "('a,bool) rbt"
> end
> 
> record 'a use_rbt_B = 
>  bar :: "'a use_rbt_A"
> 
> record 'a use_rbt_C = 
>  com :: "('a,bool)rbt"
> 
> end





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