Irvin

There is a list_max defined in miscTheory. It is identical to MAX_LIST in rich_listTheory. All uses of it should migrate to using MAX_LIST defined in richList and it should be...

Right now when cakeml is given the program of the form ``` fun const_optimization x = case x of A a => 10 | B a b => 10 |...

when cakeml is given ``` fun evaluated_case_elim x = case x of A a => A a | B a b => B a b | C a b c...

Tactictoe selftests seem to fail.

1

Despite the tests not failing the output log seems like they are ``` ttt_rewrite_thy: ConseqConv path/to/hol/src/quantHeuristics/ConseqConvScript.sml 6 proofs recognized ttt_rewrite_thy time: 0.0164 ttt_record_thy: ConseqConv path/to/hol/src/quantHeuristics/ConseqConvScript.sml cp: cannot stat 'path/to/hol/src/quantHeuristics/ConseqConvTheory.sml': No...

Implement net mapping relations to congprocs/weakenprocs for performance

1

Currently the simplifier has an performance issue in descending down terms. Where for each level of descent for every CONGPROC registered even before it matches it calls ``` if not...

Add STRIP_ALL_THEN and CHOOSE_ALL_THEN

1

Add STRIP_ALL_THEN and CHOOSE_ALL_THEN Only STRIP_ALL_THEN is exposed in the signature. STRIP_ALL_THEN should behave like REPEAT_TCL STRIP_THM_THEN and CHOOSE_ALL_THEN should behave like REPEAT_TCL CHOOSE_THEN This change is intended to speedup...

Given a term like this ``?q r. ?r q. (n' = q * m + r) /\ r < m`` Calling strip_exists on results in ``` `[“q'”, “r'”, “r”, “q”],...

We should be using LRAT for proof reconstruction for HOLSat instead of a range of not updated sat solvers with their own proof format. Note that @tanyongkiam mentions that hol-light[1]...