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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
