Irvin
Irvin
Currently list append is by default normalized left i.e. `xs ++ (ys ++ zs) = (xs ++ ys) ++ zs` This issue is about making it the opposite i.e. `(xs...
There are a bunch of files in examples/miller/formalize prefixed with extra i.e. ``` extra_boolScript.sml extra_listScript.sml extra_numScript.sml extra_pred_setScript.sml extra_realScript.sml ``` This issue is taking the theorems there, upstreaming whatever is useful...
Currently the check to filter out a net by name in the simplifier is complicated and slow https://github.com/HOL-Theorem-Prover/HOL/blob/24e40cd1c7f7e235a5c9f32f692c0d9ae04ddb2b/src/simp/src/simpLib.sml#L272C1-L275C66 ``` val checknamepart = patbase = ssnm orelse "rewrite:" ^ patbase =...
This issue is about removing the use of Rsyntax (*record syntax*) and using paired syntax which is the default. Note: This issue is only about removing the use from the...
https://github.com/HOL-Theorem-Prover/HOL/blob/24e40cd1c7f7e235a5c9f32f692c0d9ae04ddb2b/src/1/Drule.sml#L1802C1-L1804C71 HO_PART_MATCH calls free_vars. `Term.free_vars` is much slower than `Term.FVL`. This might just be replacing `free_vars bod` with `HOLset.listItems (FVL [bod])` if the order doesn't matter.
This issue is about speeding up the code in src/simp/src/Cache.sml which is causing performance problem in large theories. The solution could be a more efficient algorithm or a cache eviction...
As in title.
Metis can't prove this 2 theorems ``` METIS_PROVE[]``$? $¬`` (*Fails*) METIS_PROVE []``¬$! $¬`` (*Fails*) ``` This is **not** an issue with metis but with the encoder. metis can prove the...
Lean has recently officially announced grind. It would be good to have a similar tactic. A good start should probably be just porting over old HOL work by boulton https://link.springer.com/chapter/10.1007/3-540-60275-5_58
It would be useful if `bin/build -t3` can track which bits of the HOL repo has bit rotted.