Hello,
I have some proofs that I could previously solve by running EVAL_TAC,
after modifying computeLib.the_compset with
val _ = computeLib.del_funs [sptreeTheory.subspt_def]
val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER,
sptreeTheory.subspt_eq]
As it turns out, the proofs still run fine when interactively run in an
HOL4 emacs session, but the proofs fail when run on the command line.
The failure either is
HOL_ERR {message = "", origin_function = "Mk_comb", origin_structure = "T$
m"}
Uncaught exception: HOL_ERR {message = "", origin_function =
"Mk_comb", origin_structure = "Thm"}
or
(∀k.
k = 1 ∨ k = 0 ⇒
lookup k (BS (BN LN (LS ())) () (LS ())) =
lookup k (BS LN () (LS ())))
Previously it sufficed to have a file myComputeLib.sml declaring the
structure myComputeLib and adding the two val statements above there and
loading that file when doing the proof with "open". When trying to debug
this issue, I moved the val statements in a separate tactic, declaring
val my_eval_tac =
let
val _ = computeLib.del_funs [sptreeTheory.subspt_def]
val _ = computeLib.add_funs [realTheory.REAL_INV_1OVER,
sptreeTheory.subspt_eq]
in
EVAL_TAC
end;
but that did not solve my problem either.
Can someone help me resolve this or give me a hint on how to debug this
issue?
Thanks,
Heiko
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
