		Search-engine friendly clone of the ACL2 documentation.

Definition

Make-definition

Basic constructor macro for definition structures.

Syntax

(make-definition [:name <name>] 
                 [:para <para>] 
                 [:body <body>])

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

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

Definition

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

Macro: make-definition

(defmacro make-definition (&rest args)
  (std::make-aggregate 'definition
                       args '((:name) (:para) (:body))
                       'make-definition
                       nil))

Function: definition

(defun definition (name para body)
  (declare (xargs :guard (and (stringp name)
                              (string-listp para)
                              (constraint-listp body))))
  (declare (xargs :guard t))
  (let ((__function__ 'definition))
    (declare (ignorable __function__))
    (b* ((name (mbe :logic (str-fix name) :exec name))
         (para (mbe :logic (string-list-fix para)
                    :exec para))
         (body (mbe :logic (constraint-list-fix body)
                    :exec body)))
      (cons :definition (list (cons 'name name)
                              (cons 'para para)
                              (cons 'body body))))))