Re: [isabelle] Types for Function.get_info
I discovered that when defining a function in Isabelle/HOL, as soon as the
type variables of the type annotation differs from the ones of the infered
type (without type annotation), the function is added twice (with these two
typing informations) to the FunctionData.
Bug or feature ?
I confirm that this is a bug in function's way of declaring its data.
After the termination proof, the data is updated by just re-issuing the
declaration, but the termination part has a different typing than the
function part, even if they come from the same thing originally.
It is not really easy to do this right in the presence of arbitrary
local theory magic... I'll have a look at some point (I hope it is not a
show-stopper for you).
This archive was generated by a fusion of
Pipermail (Mailman edition) and