Thanks a lot.
On Thursday, March 27, 2014 12:48 AM, Michael Norrish
<[email protected]> wrote:
1. The simplest way would be to put your overloads and abbreviations into a
base theory that your subsequent theories all import. If you must have these
parser changes in a lib file, then this is possible, but you should change the
commands so that they are all "temp" versions. I.e., instead of overload_on,
write temp_overload_on, and instead of type_abbrev, write temp_type_abbrev.
Lib files do not need to have signatures, so you could just create an
oprLib.sml file that was of the shape
structure oprLib = struct ... end
To make sure that Holmake includes this, you need to put
open oprLib
Into your source file.
2. The simpset types are all visible in simpLib.sig: you will want
simpLib.simpset and/or simpLib.ssfrag
Michael
On 27 Mar 2014, at 6:56, "hamed nemati"
<[email protected]<mailto:[email protected]>> wrote:
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]<mailto:[email protected]>
https://lists.sourceforge.net/lists/listinfo/hol-info
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
------------------------------------------------------------------------------
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------------------------------------------------------------------------------
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
