Re: [isabelle] Strange eta-expansion on induction



Eta-expansion is an intrinsic part of the higher-order unification algorithm. Following each unification by an eta-contraction step would be inefficient, and equally arbitrary. The “problem" that must be “fixed" is any code that cannot exist with this basic fact of nature.

Larry Paulson


On 1 Mar 2012, at 20:15, Brian Huffman wrote:

> I have complained at length about this issue before. See this thread
> from August of last year:
> 
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-August/msg00080.html
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2011-August/msg00089.html
> 
> To summarize: In my opinion, having a proof kernel that does
> eta-expansion willy-nilly is an embarrassment; I also have similar
> feelings about the "eta-contract" option in the pretty-printer, which
> our eta-expanding kernel makes necessary.
> 
> Unfortunately, fixing the problem properly would require modifying the
> unification code in the kernel, which hardly anybody understands. It
> would be hard to get anyone to trust a modified version of it.






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