Am 17.06.2016 4:04 nachm. schrieb "Mark Adams" :
>
> I think the problem now is that the syntactic form of the HOL term you
supply to 'new_inductive_definition' does not fit what is allowed by the
command, because you are not allowed to have compound implications (see the
HOL Light reference manual
I think the problem now is that the syntactic form of the HOL term you
supply to 'new_inductive_definition' does not fit what is allowed by the
command, because you are not allowed to have compound implications (see
the HOL Light reference manual entry for 'new_inductive_definition').
So I think y
Hello,
On 06/16/2016 01:45 PM, Mark Adams wrote:
Hi Heiko,
That's strange, your corrected version goes through fine on my
computer. Do you still get the same problem if you restart HOL Light
and enter the corrected script? What version of HOL Light are you using?
Mark.
It turns out,
Hi Heiko,
That's strange, your corrected version goes through fine on my computer.
Do you still get the same problem if you restart HOL Light and enter
the corrected script? What version of HOL Light are you using?
Mark.
On 16/06/2016 10:01, Heiko Becker wrote:
> Forwarded Message --
Hello Heiko,
It worked for me:
let sstep_RULES,sstep_INDUCT,sstep_CASES = new_inductive_definition
`(!x e s env v. exp_eval e env = v ==> sstep (Ass x e s) env s
(upd_env x v env)) /\
(!c s t env. bval c env = T ==> sstep (Ite c s t) env s env) /\
(!c s t env. bval c env = F ==> sstep (I
Forwarded Message
Subject:Re: [Hol-info] HOL-Light Beginner Questions
Date: Thu, 16 Jun 2016 10:59:44 +0200
From: Heiko Becker
To: Ramana Kumar
CC: hol-info
On 06/16/2016 01:57 AM, Ramana Kumar wrote:
I expect it could be because the Boolean constants
