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" <[EMAIL PROTECTED]> Cc: "Robert Boyer" <[EMAIL PROTECTED]>, [EMAIL PROTECTED], axiom-developer@nongnu.org, [EMAIL PROTECTED], "Matt Kaufmann" <[EMAIL PROTECTED]> 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 _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org http://lists.nongnu.org/mailman/listinfo/axiom-developer