Thanks for the analysis Albert.
This issue has been fixed by Anthony Fox in
e84a11e8adcc0f0dd0fc8936a7df8bf61f4f9fc5.
On Mon, Apr 14, 2014 at 8:05 PM, Albert Y. C. Lai <tre...@vex.net> wrote:
> On 14-04-14 10:26 AM, Ramana Kumar wrote:
> > Could it be that listSimps.sml is picking up EXISTS_DEF from boolTheory
> > rather than from listTheory?
> >
> > > load"listLib";
> > val it = (): unit
> > > computeLib.CBV_CONV (listLib.list_compset()) ``EXISTS P []``;
> > <<HOL message: inventing new type variable names: 'a>>
> > val it = |- EXISTS P [] ⇔ EXISTS P []: thm
>
> boolTheory.EXISTS_DEF shadowing listTheory's is half of the story. To
> see this, EVERY is a success:
>
> > computeLib.CBV_CONV (listLib.list_compset()) ``EVERY P []``;
> <<HOL message: inventing new type variable names: 'a>>
> val it = |- EVERY P [] ⇔ T: thm
>
> (This also refutes my preliminary hypothesis: I thought that the
> call-by-value flavour would hate the free variable P.)
>
> Adding listTheory.EXISTS_DEF works. But you have to be careful how
> exactly you do the adding.
>
> This adding works:
>
> > val mine = listLib.list_compset();
> val mine = <compset>: computeLib.compset
> > computeLib.add_thms [listTheory.EXISTS_DEF] mine;
> val it = (): unit
> > computeLib.CBV_CONV mine ``EXISTS P []``;
> <<HOL message: inventing new type variable names: 'a>>
> val it = |- EXISTS P [] ⇔ F: thm
>
> This adding will not work:
>
> computeLib.add_thms [listTheory.EXISTS_DEF] (listLib.list_compset());
> computeLib.CBV_CONV (listLib.list_compset()) ``EXISTS P []``;
>
> Why? Because every time list_compset() is evaluated, it builds and gives
> you a new compset from scratch. (Carefully chase down its call graph to
> see.) The adding is discarded because you don't save it and listLib
> doesn't save it either.
>
> Isn't impure functional programming exciting! You never know which
> unit->x functions are actually pure!
>
>
>
> ------------------------------------------------------------------------------
> Learn Graph Databases - Download FREE O'Reilly Book
> "Graph Databases" is the definitive new guide to graph databases and their
> applications. Written by three acclaimed leaders in the field,
> this first edition is now available. Download your free book today!
> http://p.sf.net/sfu/NeoTech
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Learn Graph Databases - Download FREE O'Reilly Book
"Graph Databases" is the definitive new guide to graph databases and their
applications. Written by three acclaimed leaders in the field,
this first edition is now available. Download your free book today!
http://p.sf.net/sfu/NeoTech
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
