		Search-engine friendly clone of the ACL2 documentation.

Fty-info

Make-fty-info

Basic constructor macro for fty-info structures.

Syntax

(make-fty-info [:name <name>] 
               [:category <category>] 
               [:type <type>] 
               [:guards <guards>] 
               [:returns <returns>])

This is the usual way to construct fty-info structures. It simply conses together a structure with the specified fields.

This macro generates a new fty-info structure from scratch. See also change-fty-info, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-fty-info

(defmacro make-fty-info (&rest args)
  (std::make-aggregate 'fty-info
                       args
                       '((:name)
                         (:category)
                         (:type)
                         (:guards)
                         (:returns))
                       'make-fty-info
                       nil))

Function: fty-info

(defun fty-info (name category type guards returns)
  (declare (xargs :guard (and (symbolp name)
                              (symbolp category)
                              (symbolp type)
                              (symbol-listp guards)
                              (symbolp returns))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'fty-info))
    (declare (ignorable acl2::__function__))
    (b* ((name (mbe :logic (symbol-fix name)
                    :exec name))
         (category (mbe :logic (symbol-fix category)
                        :exec category))
         (type (mbe :logic (symbol-fix type)
                    :exec type))
         (guards (mbe :logic (symbol-list-fix guards)
                      :exec guards))
         (returns (mbe :logic (symbol-fix returns)
                       :exec returns)))
      (list (cons 'name name)
            (cons 'category category)
            (cons 'type type)
            (cons 'guards guards)
            (cons 'returns returns)))))