[Axiom-developer] Re: [Maxima] 2.7.0 nqthm compile times

[Matt Kaufmann]

Regarding:

>> My advice: ignore user-supplied ftype declaims.

I don't have any problem with that as the default behavior.  But I'd
like to be able to override that "ignore" -- that's what I was trying
to say in this part of my reply yesterday (where here I've tried to
eliminate some ambiguity in it).

  As you know, in ACL2 we do our own auto-proclaiming of function types.
  Just to be safe, I think it would be good if there were a way to turn
  off the auto-proclamation capability, as a way to work around any
      ^^^
     GCL's
  problems we might encounter, using our own proclaiming instead.
                               ^^^^^^^^^^^^^
                              by using ACL2's

Thanks --
-- Matt
   DKIM-Signature: a=rsa-sha1; c=relaxed/relaxed;
           d=gmail.com; s=beta;
           
h=domainkey-signature:received:received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references;
           
b=VZiMC3HyT3UTewJZPY62wUlvOIzW8bNMIqcj7N7aoKMfRvx+L4OTSj0xu9lgHRjiOx8V4XriJpjyz5XbyEPEWWzOSbBIt1+DzVEotW9L/N7m8hFUewXaZIyHxb2JEl2bdM/Lms7XjA4u0qWKL4WOcfG0euxAmYNEmStO2MklU3Y=
   DomainKey-Signature: a=rsa-sha1; c=nofws;
           d=gmail.com; s=beta;
           
h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references;
           
b=Uc7KjbTveZ5Y+baAcGZZ+FkahsWXBfq25sEF599pvFHDLdFq/ZCNUJWflqsNaRltPGEdYCNVtW6EW8zr4bUbf5IGM5N8J9BbzKGWSj6Va3qC3KFjA31NtFJe7ShtugO6Ys0hWjTy+SiDbmLNAl30ImZOZk7id3U/8HeSjR+9t8M=
   Date: Mon, 25 Jun 2007 09:03:49 -0600
   From: "Robert Dodier" <address@hidden>
   Cc: "Robert Boyer" <address@hidden>, address@hidden,
           address@hidden, address@hidden,
           "Matt Kaufmann" <address@hidden>
   Content-Disposition: inline
   X-SpamAssassin-Status: No, hits=-1.8 required=5.0
   X-UTCS-Spam-Status: No, hits=-163 required=200

   Camm,

   Thanks a lot for your work on GCL.

   My only comment about recompiling policy is that I hope that
   the system remains in a safe state by default.

   About this,

   > A final question remains of
   > whether or not to actually use ftype declaims if provided.

   My advice: ignore user-supplied ftype declaims.

   All the best, & keep up the good work.

   Robert Dodier