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" <robert.dodier at gmail.com>
Cc: "Robert Boyer" <boyer at cs.utexas.edu>, maxima at math.utexas.edu,
axiom-developer at nongnu.org, gcl-devel at gnu.org,
"Matt Kaufmann" <kaufmann at cs.utexas.edu>
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