Here's the diff that you provided to address my proclaim problem. This is in addition to the diff that you provided in
http://mail.gnu.org/archive/html/gcl-devel/2003-09/msg00137.html to address Dave Greve's original report of a proclaim problem.
--- gcl_predlib.lsp 2003-11-06 21:53:19.000000000 -0500
+++ /tmp/f.lisp 2003-12-05 19:25:07.000000000 -0500
@@ -261,9 +261,8 @@ (defun normalize-type (type &aux tp i )
;; Loops until the car of type has no DEFTYPE definition.
(when (and (consp type) (eq (car type) 'satisfies)) - (unless (setq tp (get (cadr type) 'predicate-type))
- (error "Cannot process type ~S~%" type))
- (setq type tp))
+ (when (setq tp (get (cadr type) 'predicate-type))
+ (setq type tp))) (loop
(if (atom type) (setq tp type i nil)
> 2) I'd like to make sure that Paul agrees that handling user-defined > predicates in a (satisfies...) type type specifier in this manner > is acceptable (or even proper).
I believe it's acceptable given the current use we're making of it in ACL2, i.e. in guard proofs. We don't need the user-defined predicate satisfaction information to be available in order to optimize code generation, for instance. But, I'm no Common Lisp language lawyer, so I have no clue as to what's actually required for this case.
BTW, earlier GCL's, i.e. GCL 2.2.2, handled this situation adequately for our needs. I don't know if any additional wisdom could be found by looking back at that version of the source.