HOL

HOL copied to clipboard

It is not uncommon to have a theory file which proves a single, relatively clean theorem - but the purpose of the file is cluttered by various intermediate definition and...

hrutvik

Reinstate Reference Manual's list of theorems

1

The Reference manual used to include a big list of the core system's theorems. I found this useful when I was learning HOL, so perhaps we should try to do...

mn200

Hi, I have my `HOL4_YICES_EXECUTABLE` environment variable set to Yices 1.0.40 since many years ago. I never actually use Yices to do anything: ``` $ echo $HOL4_YICES_EXECUTABLE /Users/binghe/ML/yices-1.0.40/bin/yices ``` Usually...

binghe

Handle rewrites with new vars on r.h.s. that appear in conditions

2

A conditional rewrite theorem of the form P a b ==> f a = g b is usually useless to the simplifier and ignored as a result. However, it could...

mn200

lex-errors about unterminated comments should report start position

1

Holmake reports the error but tells the user it occurs at the end of the file. It would be much more helpful if it reported the location of the unmatched...

mn200

Bad type error message in presence of overloading

1

E.g.: ``` ``(GENLIST (++) n = GENLIST f) n``; Exception- HOL_ERR {message = "on line 3, characters 10-13:\nCouldn't infer type for overloaded name ++", origin_function = "type-analysis", origin_structure = "Preterm"}...

mn200

HOL_ERR to pick up term and type arguments

11

Change the fundamental exception to give exception-raisers the option of attaching relevant terms and types. For the sake of backwards compatibility, we can redefine helpers like `mk_HOL_ERR` and friends (creating...

mn200

Sharing & memory consumption after theory load

15

The SharingTables structure is used to compress the terms and types that appear in a theory's signature. The compression ensures that repeated terms and types are only stored once. This...

talsewell

Arithmetic normalisation of subtraction + SUC doesn't

1

If `0 < x` is in the assumptions `simp[]` still won't prove `f (SUC (x-1)) = f x`

mn200

Pattern-matching compilation fails

1

With the "classic" heuristic, this works. Now, with the new default, it fails (with an exception about missing cases): ``` val foo_def = Define` (foo 0 0 0 = 0)...

mn200