match_mp_tac is indeed causing an error because it is not applicable in the
other subgoals.
Michael
From: Waqar Ahmad via hol-info
Reply-To: Waqar Ahmad <12phdwah...@seecs.edu.pk>
Date: Friday, 21 September 2018 at 08:39
To: "konrad.sl...@gmail.com"
Cc: hol-info
Subject: Re: [Hol-info] assump
As Thomas said, you are probably encountering this use of temporary files for
the first time. In particular, I suppose you may not have tried to cut and
paste large regions of your script file in the past. You could confirm that
this is the problem by seeing if smaller regions of text do trans
ITP2019: Interactive Theorem Proving, Tenth International Conference
September 8-13 2019, Portland, OR, USA
http://itp19.cecs.pdx.edu
it...@cecs.pdx.edu
CALL FO
Hi,
Thanks for the reply. I think the match_mp_tac is causing the error since
if I only pop the assumption the tactic works on first subgoal.
rw [] \\ (pop_assum (mp_tac)) THEN_LT SPLIT_LT 1 (ALL_LT, ALLGOALS (rw[]))
> val it =
SG3
A1 ==> B1
Seems like the rw[] is breaking the proof into 3 subgoals, and only on the
first one is the pop_assum match_mp_tac succeeding. So the proof is failing
before it gets to the THEN_LT.
Konrad.
On Thu, Sep 20, 2018 at 2:05 PM Waqar Ahmad via hol-info <
hol-info@lists.sourceforge.net> wrote:
> Hi,
>
Hi,
thank you for your reply.
I am using an oracle virtual machine on my laptop
running ubuntu-16.04.4-desktop-i386. I have been using this machine for
about three months now, and I have not had any problem until yesterday.
Best Regards,
Yassmeen
On Thu, Sep 20, 2018 at 5:25 PM, Thomas Tuerk
Hi,
I believe this is due to how hol-mode copies input from emacs buffers to
HOL. Look at HOL-DIR/tools/hol-mode.el line 802 ff.
(https://github.com/HOL-Theorem-Prover/HOL/blob/master/tools/hol-mode.src#L800).
If a chunk of text you want to send exceeds a certain size, it is
written to a temp-file
Hi,
I'm trying to use the tactical SPLIT_LT to multiple subgoals. However, I'm
facing error with assumption matching. For instance, I've a proof goal of
this form:
`(A1 ==> B1) ==> (B1 /\ SG2 /\ SG3)`
rw []
\\ (pop_assum (fn th => match_mp_tac th)) THEN_LT SPLIT_LT 1 (ALL_LT,
ALLGOALS (rw[]))
I
Hi,
Sorry for sending this email again, but it seems that there was a problem
with the first email
I am using HOL4, yesterday I started receiving this error message
Exception raised Io {cause = SysErr ("No such file or directory", SOME
ENOENT), function = "TextIO.openIn", name = "/tmp/hol2207zVM
Hi,
I am using HOL4, yesterday I started receiving this error message
Exception raised Io {cause = SysErr ("No such file or directory", SOME
ENOENT), function = "TextIO.openIn", name = "/tmp/hol2207zVM"}
I am using HOL4 in the hol-mode, but when I use HOL directly using the
shell, my script runs
Hi,
I am using HOL4 in hol-mode, yesterday I started receiving this error
message
___
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
**
The 22nd International Conference on
Logic for Programming, Artificial Intelligence and Reasoning
LPAR-22
Haile Resort, Awas
12 matches
Mail list logo
