Re: [Gcl-devel] Re: Chasing down a compiler bug

[Matt Kaufmann]

Camm --

Unofficially, yes.  But you can corrupt ACL2 that way, so if you are thinking
of ACL2 as a theorem prover, then defining things in raw Lisp is a problem.
(You can also :SET-RAW-MODE T instead of :Q if you want to do arbitrary defuns,
and you'll get a message to that effect.)

But for just hacking around I do :q and then (compile (defun ...)) all the
time.

-- Matt
   Cc: address@hidden, address@hidden
   From: Camm Maguire <address@hidden>
   Date: 24 Feb 2004 21:14:06 -0500
   User-Agent: Gnus/5.09 (Gnus v5.9.0) Emacs/21.2
   Content-Type: text/plain; charset=us-ascii

   Greetings, and thanks again!

   Matt Kaufmann <address@hidden> writes:

   > Hi, Camm --
   > 
   > You're welcome, and sorry about the defect in my reply; I was imagining 
that
   > you would replace the definition in raw Lisp.  The problem is that ACL2 
doesn't
                                         ^^^^^^^^
   Does this mean that I can just :q at the acl2 rpl and defun whatever
   lisp I want?

   Take care,


   -- 
   Camm Maguire                                         address@hidden
   ==========================================================================
   "The earth is but one country, and mankind its citizens."  --  Baha'u'llah