[isabelle-dev] Problem with transfer method
huffman.brian.c at gmail.com
Tue Oct 1 01:14:09 CEST 2013
On Mon, Sep 30, 2013 at 2:34 PM, Makarius <makarius at sketis.net> wrote:
> According to the normal context discipline, free variables are always fixed,
> like a local const. We have a few tools that violate that principle and
> consequently cause confusion, e.g. the Simplifier. There are sometimes
> historical reasons for that, and little hope for reforms.
> Is this also the case for transfer?
If you're asking whether transfer distinguishes the term constructors
Free and Const, then the answer is yes. Transfer may generalize a Free
(according to the heuristic) but will never generalize over a Const.
With more and more localized tools using Frees as constants, perhaps
it would be more robust for transfer to treat Free and Const exactly
the same. I will have to think more about this.
More information about the isabelle-dev