		Search-engine friendly clone of the ACL2 documentation.

Rule

Make-rule

Basic constructor macro for rule structures.

Syntax

(make-rule [:name <name>] 
           [:incremental <incremental>] 
           [:definiens <definiens>])

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

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

Definition

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

Macro: make-rule

(defmacro make-rule (&rest args)
  (std::make-aggregate 'rule
                       args
                       '((:name) (:incremental) (:definiens))
                       'make-rule
                       nil))

Function: rule

(defun rule (name incremental definiens)
  (declare (xargs :guard (and (rulenamep name)
                              (booleanp incremental)
                              (alternationp definiens))))
  (declare (xargs :guard t))
  (let ((__function__ 'rule))
    (declare (ignorable __function__))
    (b* ((name (mbe :logic (rulename-fix name)
                    :exec name))
         (incremental (mbe :logic (acl2::bool-fix incremental)
                           :exec incremental))
         (definiens (mbe :logic (alternation-fix definiens)
                         :exec definiens)))
      (cons :rule (list name incremental definiens)))))