		Search-engine friendly clone of the ACL2 documentation.

Fundef

Make-fundef

Basic constructor macro for fundef structures.

Syntax

(make-fundef [:extension <extension>] 
             [:specs <specs>] 
             [:declor <declor>] 
             [:asm? <asm?>] 
             [:attribs <attribs>] 
             [:declons <declons>] 
             [:body <body>] 
             [:info <info>])

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

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

Definition

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

Macro: make-fundef

(defmacro make-fundef (&rest args)
  (std::make-aggregate 'fundef
                       args
                       '((:extension)
                         (:specs)
                         (:declor)
                         (:asm?)
                         (:attribs)
                         (:declons)
                         (:body)
                         (:info))
                       'make-fundef
                       nil))

Function: fundef

(defun fundef (extension specs
                         declor asm? attribs declons body info)
  (declare (xargs :guard (and (booleanp extension)
                              (decl-spec-listp specs)
                              (declorp declor)
                              (asm-name-spec-optionp asm?)
                              (attrib-spec-listp attribs)
                              (declon-listp declons)
                              (comp-stmtp body)
                              (acl2::any-p info))))
  (declare (xargs :guard t))
  (b* ((extension (mbe :logic (bool-fix extension)
                       :exec extension))
       (specs (mbe :logic (decl-spec-list-fix specs)
                   :exec specs))
       (declor (mbe :logic (declor-fix declor)
                    :exec declor))
       (asm? (mbe :logic (asm-name-spec-option-fix asm?)
                  :exec asm?))
       (attribs (mbe :logic (attrib-spec-list-fix attribs)
                     :exec attribs))
       (declons (mbe :logic (declon-list-fix declons)
                     :exec declons))
       (body (mbe :logic (comp-stmt-fix body)
                  :exec body))
       (info (mbe :logic (identity info)
                  :exec info)))
    (cons (cons (cons extension specs)
                (cons declor asm?))
          (cons (cons attribs declons)
                (cons body info)))))