Hi Behzad,
A 6000 line term is probably making the parser and/or
type inferencer work very hard. It might be better to
build the term using term constructors such as
mk_neg, mk_conj, mk_disj, mk_exists, etc.
Cheers,
Konrad.
On Sep 16, 2009, at 6:56 PM, Behzad Akbarpour wrote:
> Hi everyone;
Hi everyone;
I have a huge definition of an RTL design function (more that 6000 lines of
HOL code), and I'm trying to load and compile it in HOL, but I couldn't
succeed. I first tried to copy and paste from emacs but it didn't work.
Then, I made a script file out of the definition together with
I attach a Call for Abstracts for the "Designing Correct Circuits"
workshop to be held next March in Cyprus as a satellite event of
ETAPS2010.
I would be most grateful if you would bring it to the attention of any
colleagues and friends who might be interested -- and, please,
consider submitting
- Sorry for cross-postings -
- 4 days left before paper submission deadline -
The 5th International Conference on Signal Image Technology and Internet Based
Systems (SITIS'09)
