Deftrans-defn-const-expr-option
- Signature
(deftrans-defn-const-expr-option 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-const-expr-option
(defun deftrans-defn-const-expr-option
(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-const-expr-option))
(declare (ignorable __function__))
(deftrans-defn
'const-expr-option
names bodies
'((const-expr? const-expr-optionp))
extra-args
(cons 'const-expr-option-case
(cons 'const-expr?
(cons ':some
(cons (cons (cdr (assoc-eq 'const-expr names))
(cons 'const-expr?.val
extra-args-names))
'(:none nil)))))
'(:returns (new-const-expr? const-expr-optionp)
:measure (const-expr-option-count const-expr?)))))
