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
