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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
