HOL

HOL copied to clipboard

This is due to the use of "magic" constants to stand for various components of the case expression before it is translated into its final form.

mn200

tactic application cache

3

The proof manager could keep a cache of previously seen and proved subgoals, and prove them immediately if they are seen again. This might speed up interactive development with long-running...

xrchz

Holmake to rebuild based on theory hashes rather than timestamps

3

This would for example avoid cascading rebuilds if you just add a comment to a script file (and it produces exactly the same theory).

xrchz

E.g., turn a theorem like 0 < x ** y .... into 1

mn200

As per this comment to `hol-info` by John Harrison: > HOL Light has a variant of the inductive relation command called "new_inductive_set" (written by Marco Maggesi) that lets you express...

mn200

Consider inverting sense of parenthesis-style directive ParoundPrec

2

Currently the documentation says: > The `ParoundPrec` value [...] causes parentheses to be added when the term is the argument to a function with a different precedence level. The code...

mn200

Holmakefile options per directory only

2

I notice that if one has `CLINE_OPTIONS` in the `Holmakefile` set to `-j1`, then this is propagated to recursive `Holmake` calls in `INCLUDES` directories as well. I guess this fits...

xrchz

The normalisation process used in `ARITH` treats something like n = 10 \/ n = 9 \/ n = 8 ... \/ n = 0 extremely badly, creating a term...

mn200

mn200

Hello. The feature requested is to add a command-line flag to Holmake to print timing information (and optionally, the number of primitive inferences performed) for each “relevant” theorem proved. I...

marioxcc