HOL

HOL copied to clipboard

One would hope `ListConv1.ALL_EL_CONV` to be an efficient specialised conversion for evaluating `EVERY _ _` terms, but it actually performs much worse than `EVAL`. If it can't be made to...

xrchz

Emacs hangs when using mark tactic twice or inside a term

2

Hi, Using mark tactic (M-h t) twice in a row hangs emacs, recoverable by (C-g g). Using mark tactic inside a term, such as when the cursor is on h...

Luceat

Make Unwind work with some

1

There's a theorem roughly like ``` (some x. (x = v) /\ P(x)) = if P(v) then SOME v else NONE ``` that should be used in the simplifier's unwind...

mn200

Handle paired-abstractions better

4

In particular, if there is a quantifier over a variable of pair type, and that same variable is an argument to a paired abstraction, then the quantifier should be rewritten...

mn200

New Representation for Pattern Matches - Extra Features

1

This is a subtask of issue #285. Implement extra features for pattern matches. Current ideas: - improved support for arithmetic expressions - improved support for list patterns - better support...

thtuerk

Starting a new subgoal (`by` or `suffices_by`) without selecting the exact term first (and just picking it up on the line) correctly strips off text after the term, but keeps...

xrchz

More precise control of Holmake --fast

1

When running a Holmake --fast on a project that relies on unbuilt theories in HOL's own examples directory, it builds those theories cheated, which affects other projects where you might...

SOwens

 As _per_ picture, we think we have a story for the creation and use of articles that assert axioms, constants and types, and then prove consequences thereof. We can...

mn200

The default behaviour of the simplifier (_i.e._, with `srw_ss()`) doesn't adjust the following: ``` f((x:int) - 2 + 1) ``` There doesn't seem much reason to leave terms like this...

mn200

When writing docfiles documentation, one should typically write some examples to illustrate how to use the function being documented. Currently, these must be written entirely manually. They would benefit from...

xrchz