When <holdir>/bin/hol starts up, it is sitting on top of a somewhat
ad hoc collection of theories:
> ancestry"-";
val it =
["ConseqConv", "quantHeuristics", "patternMatches", "ind_type", "while",
"one", "sum", "option", "pair", "combin", "sat", "normalForms",
"relation", "min", "bool", "marker", "num", "prim_rec", "arithmetic",
"numeral", "basicSize", "numpair", "pred_set", "list", "rich_list",
"indexedLists"]: string list
Some of these are support for other proof infrastructure, but the main
theories give you booleans, products, sums, options, numbers, lists,
and sets. This is a useful basis on which to begin most formalizations.
But if you want to have a minimal ancestry for your theory, you could try
building on <holdir>/bin/hol.bare which has very little:
> ancestry"-";
val it = ["min", "bool"]: string list
Then you will have to explicitly load in all the needed tools and theories.
For use of Holmake, I am pretty sure there is an option to support
hol.bare,
but I am not sure what it is.
Konrad.
On Sun, Oct 22, 2017 at 10:01 AM, Mario Castelán Castro <
marioxcc...@yandex.com> wrote:
> Hello.
>
> When I process the following file with Holmake from a recent Git build I
> get indexedLists and patternMatches as parents; with Kananaskis-11 I get
> quantHeuristics and rich_list as parents. Why? There is no apparent
> dependency on anything but the bool theory.
>
> “open HolKernel Parse boolLib boolTheory;
> val _ = new_theory "test";
> save_thm("T", TRUTH);
> val _ = export_theory ();”
>
> --
> Do not eat animals; respect them as you respect people.
> https://duckduckgo.com/?q=how+to+(become+OR+eat)+vegan
>
>
> ------------------------------------------------------------
> ------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
