		Search-engine friendly clone of the ACL2 documentation.

Fundef

Make-fundef

Basic constructor macro for fundef structures.

Syntax

(make-fundef [:extension <extension>] 
             [:spec <spec>] 
             [:declor <declor>] 
             [:asm? <asm?>] 
             [:attribs <attribs>] 
             [:decls <decls>] 
             [:body <body>])

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)
                         (:spec)
                         (:declor)
                         (:asm?)
                         (:attribs)
                         (:decls)
                         (:body))
                       'make-fundef
                       nil))

Function: fundef

(defun fundef (extension spec declor asm? attribs decls body)
  (declare (xargs :guard (and (booleanp extension)
                              (decl-spec-listp spec)
                              (declorp declor)
                              (asm-name-spec-optionp asm?)
                              (attrib-spec-listp attribs)
                              (decl-listp decls)
                              (stmtp body))))
  (declare (xargs :guard t))
  (let ((__function__ 'fundef))
    (declare (ignorable __function__))
    (b* ((extension (mbe :logic (bool-fix extension)
                         :exec extension))
         (spec (mbe :logic (decl-spec-list-fix spec)
                    :exec spec))
         (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))
         (decls (mbe :logic (decl-list-fix decls)
                     :exec decls))
         (body (mbe :logic (stmt-fix body)
                    :exec body)))
      (list (cons 'extension extension)
            (cons 'spec spec)
            (cons 'declor declor)
            (cons 'asm? asm?)
            (cons 'attribs attribs)
            (cons 'decls decls)
            (cons 'body body)))))