Thanks Chun Tian,
I can reproduce the issue.
I tried finding out which theorems were causing the failure. They're rather
ugly (I will paste at the end of this email), but they look like valid
inputs to the "trans" function to me. It could be something to do with the
fact that some of the constant
Hi again,
The issue happens because of the following mini theory with just one datatype
definition:
open HolKernel Parse boolLib bossLib;
val _ = new_theory "Test”;
val _ = Datatype `Dertree = Der 'a (Dertree list)`;
val _ = export_theory ();
Error outputs:
FATAL ERROR: opentheory failed:
Hi Ramana,
Thanks for your detailed explanation. For your question about what am I
planning to do with the ot files, to be honest I have no plan. If I understand
OpenTheory correctly, the theory I developed may be able to run in HOL light
and Isabelle without full porting work, but currently I
(Apologies for multiple copies. Please redistribute)
*** CALL FOR PAPERS ***
ARCADE http://www.cs.man.ac.uk/~regerg/arcade/
Automated Reasoning:
Challenges, Applications, Directions, Exemplary achiev
*** DEADLINE EXTENSION ***
9th Working Conference on Verified Software:
Theories, Tools, and Experiments (VSTTE)
https://vstte17.lri.fr
July 22-23, 2017, Heidelberg, Germany
Co-located with the 29th Inte
Hi Chun Tian,
It's hard to know exactly what's wrong, but I expect there's a bug in the
OpenTheory proof recording facility of HOL4, which is implemented in
src/opentheory/postbool/Logging.sml.
When you ask Holmake to generate an .ot.art file it first generates a raw
.art file by recording all th
Hi Dwi,
I would expect that a
ASM_REWRITE_TAC[]
does the trick. It would take the assumptions as a rewrite and use it to
simplify the goal. In this case, it should simplify the goal to "!s0.
Next s0 x = Next s0 x" which is solved thanks to reflexivity. A problem
might be free type variables, i.
Hi,
I have a question,
What tactic I should use to solve this problem?
!s0. flipslv (flipslv (Next s0 x)) = Next s0 x
--
x. flipslv (flipslv x) = x
The flipslv function is just simply reverses x which is a slv datatype.
The datatype declaration is wri
