Could it be that listSimps.sml is picking up EXISTS_DEF from boolTheory
rather than from listTheory?
On Mon, Apr 14, 2014 at 3:16 PM, Ramana Kumar <ramana.ku...@cl.cam.ac.uk>wrote:
> I find this very counterintuitive:
>
> > 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
>
> whereas:
>
> > EVAL ``EXISTS P []``;
> <<HOL message: inventing new type variable names: 'a>>
> val it = |- EXISTS P [] ⇔ F: thm
>
> I also don't understand why it is happening.
> Based on how list_compset is defined, it should reduce the term like EVAL
> does.
>
> Any ideas?
>
------------------------------------------------------------------------------
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
