[isabelle-dev] a problem with interpretations in FinFun
kuncar at in.tum.de
Wed May 15 10:52:01 CEST 2013
This refers to 68c163598f07 + my local patches in Lifting/Transfer.
During testing my local patches, I found out that I broke the theory
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
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)
But now I get this:
(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.
More information about the isabelle-dev