Hello everyone,
Following are two simple questions related to Holmake.
1 - Suppose we have a file containing a number of type abbreviations
(type_abbrev) and overloaded operators (overload_on), lets call it oprLib, and
we have another file that contains theorems, depending on those abbreviated
types and operators. Then the question is that how we can load oprLib in the
file containing theorems such that this file can be compiled by Holmake. I
tried to create a Lib file but I do not know exactly what the .sig file for
this library should look like! I also look at the Hol4 source but I could not
find any example related to this issue. Is there any way, other than putting
all these abbreviations in the theorems source file, to load oprLib?
Here is an example of abbreviations I am using:
val _ = type_abbrev("mem", ``:bool[32]->bool[8]``);
val _ = overload_on ("w+", Term`$word_add`);
val _ = set_fixity "w+" (Infixl 600);
2 - what is the signature for a simpset in Lib file? for example val let_ss =
simpLib.mk_simpset [boolSimps.LET_ss];
Thanks in advance.------------------------------------------------------------------------------
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/13534_NeoTech
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
