On 22/10/17 17:54, michael.norr...@data61.csiro.au wrote:
> We don’t track logical dependencies. Rather, we record what theories have
> been loaded. […]
>
> Both the command-line --holstate= and Holmakefile HOLHEAP= methods seem fine
> to me. […]
Thanks for the answer.
--
Do not eat animals;
We don’t track logical dependencies. Rather, we record what theories have been
loaded. This loading is “irreversible”, so using the default setup will force
you to have all those theories as ancestors.
Both the command-line --holstate= and Holmakefile HOLHEAP= methods seem fine to
me. Using
On 22/10/17 13:04, Konrad Slind wrote:
> 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.
Thanks. I thought “export_theory”
When /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",
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
