|
|
|---|
|
|
|
|---|
Construct a name.
This macro accepts one or two arguments. If one argument is passed, it must be a string, and the macro returns a simple name containing that string. If two arguments are passed, they must be a string and a natural number, and the macro returns an indexed name containing the string and natural number.
Macro:
(defmacro pfname (&rest args) (declare (xargs :guard (and (consp args) (or (endp (cdr args)) (and (consp (cdr args)) (endp (cddr args))))))) (if (consp (cdr args)) (cons 'name-indexed (cons (car args) (cons (cadr args) 'nil))) (cons 'name-simple (cons (car args) 'nil))))