Irvin
Irvin
Note that difficulty of this is that opentheory could break.
Given a term of the form `Abs(Fv("x",_),(Abs(Fv("x",_),_)` Calling strip_abs on it differs from repeatedly calling dest_abs on it. See this example ``` val abs = mk_abs (``x':bool``,mk_abs (``x:bool``,``x /\ x'``))...
Current WORD_GROUND_CONV is set up with wildcard keys. This is results in extremely noisy simp tracing and also has performance impacts. It should be setting up multiple keys instead similar...
Also add a UNCURRY_PRED theorem and add it to AllCasePreds
Similar to how its currently true that `TL [] = []` having `FRONT [] = []` would be allow for some preconditions on theorems to be removed.
It would nice to have a listener module for term matching that can be turned on and off. The first order matcher in Term.sml wastes time in calling KernelSig.id_toString https://github.com/HOL-Theorem-Prover/HOL/blob/9a0aad85ccaf911c3b43823532a691042a0f879d/src/0/Term.sml#L909-L910...
Right now that I've found that free_varsl in Traverse.add_context(2)doit(2) is a hot path the simplifier. One issue is that variant called in EQ_CONGPROC is can show different performance on the...
SPEC_ALL is extremely slow for large terms. Using Thm.Specialize which will use lazy beta conv only helps the standard kernel. Given that GENL is already in the kernel I don't...
Right now there's a lot wasted time in code that gets the free variables of a term where Term.compare is called. This requires two checks whether the term had the...
Right now `Dep` and `Tag` are implemented using ordered lists. However their merge operator doesn't take care to prevent allocation of new lists when the two lists are pointer eq....