Deftrans-defn-structdecl
- Signature
(deftrans-defn-structdecl 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-structdecl
(defun deftrans-defn-structdecl
(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-structdecl))
(declare (ignorable __function__))
(deftrans-defn
'structdecl
names bodies '((structdecl structdeclp))
extra-args
(cons
'structdecl-case
(cons
'structdecl
(cons
':member
(cons
(cons
'make-structdecl-member
(cons
':extension
(cons
'structdecl.extension
(cons
':specqual
(cons
(cons (cdr (assoc-eq 'spec/qual-list names))
(cons 'structdecl.specqual
extra-args-names))
(cons
':declor
(cons (cons (cdr (assoc-eq 'structdeclor-list names))
(cons 'structdecl.declor
extra-args-names))
'(:attrib structdecl.attrib))))))))
(cons
':statassert
(cons (cons 'structdecl-statassert
(cons (cons (cdr (assoc-eq 'statassert names))
(cons 'structdecl.unwrap
extra-args-names))
'nil))
'(:empty (structdecl-empty))))))))
'(:returns (new-structdecl structdeclp)
:measure (structdecl-count structdecl)))))
