Re: [isabelle] Types for Function.get_info



Hi Mathieu,

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).

Thanks,
Alex





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