Deftrans-defn-initer
- Signature
(deftrans-defn-initer names bodies extra-args extra-args-names)
→
*
- Arguments
- names — Guard (alistp names).
- bodies — Guard (alistp bodies).
- extra-args — Guard (true-listp extra-args).
- extra-args-names — Guard (true-listp extra-args-names).
Definitions and Theorems
Function: deftrans-defn-initer
(defun deftrans-defn-initer
(names bodies extra-args extra-args-names)
(declare (xargs :guard (and (alistp names)
(alistp bodies)
(true-listp extra-args)
(true-listp extra-args-names))))
(let ((__function__ 'deftrans-defn-initer))
(declare (ignorable __function__))
(deftrans-defn
'initer
names bodies '((initer initerp))
extra-args
(cons
'initer-case
(cons
'initer
(cons
':single
(cons
(cons 'initer-single
(cons (cons (cdr (assoc-eq 'expr names))
(cons 'initer.expr extra-args-names))
'nil))
(cons
':list
(cons
(cons
'make-initer-list
(cons ':elems
(cons (cons (cdr (assoc-eq 'desiniter-list names))
(cons 'initer.elems extra-args-names))
'(:final-comma initer.final-comma))))
'nil))))))
'(:returns (new-initer initerp)
:measure (initer-count initer)))))
