[isabelle-dev] a problem with interpretations in FinFun

[Ondřej Kunčar]

OK, now I know the answer.
I opened Tobias's theories in HOL/IMP (because they use lift_definition) 
and this actually imports HOL/ex/Interpretation_with_Defs.thy that 
changes the global state (locale interpretations).

Tricky, but it makes sense.

Ondrej

On 05/15/2013 10:52 AM, Ondřej Kunčar wrote:
> This refers to 68c163598f07 + my local patches in Lifting/Transfer.
>
> During testing my local patches, I found out that I broke the theory
> FinFun.thy
>
> In every interpretation I got an error message "Illegal free variables
> in expression: ...". For example for the first interpretation, it was
> "b'". I don't think the error was related to my local changes since I
> didn't change anything in locales and even if I did something strange
> with contexts in lift_definition, it should be ok when we are back at
> the toplevel.
>
> I "fixed" the problem by writing "for b'" (for g and so on) for each
> interpretation. But funnily after I restarted Jedit, I cannot reproduce
> this problem any more, i.e, FinFun goes through even without these "for
> b'" additional statements.
>
> Another strange thing that might or might not be related: when I
> hovered over b' in this expression
>
> interpretation finfun_update: comp_fun_commute "λa f. f(a :: 'a $:= b')"
>
> I got originally(=in the state with the error message mentioned above)
> this type:
> free variable
> :: 'b
> But now I get this:
> free variable
> :: 'b
> :: 'b
> (i.e., 'b is there twice)
>
> Since I cannot reproduce this problem any more, might be hard to say
> anything about it, but maybe it rings a bell in somebody's head.
>
> Ondrej
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev