		Search-engine friendly clone of the ACL2 documentation.

Defdefparse-function-spec-rulename

Make-defdefparse-function-spec-rulename

Basic constructor macro for defdefparse-function-spec-rulename structures.

Syntax

(make-defdefparse-function-spec-rulename [:get <get>] 
                                         [:order <order>])

This is the usual way to construct defdefparse-function-spec-rulename structures. It simply conses together a structure with the specified fields.

This macro generates a new defdefparse-function-spec-rulename structure from scratch. See also change-defdefparse-function-spec-rulename, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-defdefparse-function-spec-rulename

(defmacro make-defdefparse-function-spec-rulename (&rest args)
  (std::make-aggregate 'defdefparse-function-spec-rulename
                       args '((:get) (:order))
                       'make-defdefparse-function-spec-rulename
                       nil))

Function: defdefparse-function-spec-rulename

(defun defdefparse-function-spec-rulename (get order)
  (declare (xargs :guard (and (common-lisp::stringp get)
                              (pos-listp order))))
  (declare (xargs :guard t))
  (let ((__function__ 'defdefparse-function-spec-rulename))
    (declare (ignorable __function__))
    (b* ((get (mbe :logic (str-fix get) :exec get))
         (order (mbe :logic (acl2::pos-list-fix order)
                     :exec order)))
      (cons :rulename (list get order)))))