		Search-engine friendly clone of the ACL2 documentation.

Driver

Make-driver

Basic constructor macro for driver structures.

Syntax

(make-driver [:value <value>] 
             [:strength <strength>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-driver

(defmacro make-driver (&rest args)
  (std::make-aggregate 'driver
                       args '((:value) (:strength . 6))
                       'make-driver
                       nil))

Function: driver

(defun driver (value strength)
  (declare (xargs :guard (and (svex-p value) (natp strength))))
  (declare (xargs :guard t))
  (let ((__function__ 'driver))
    (declare (ignorable __function__))
    (b* ((value (mbe :logic (svex-fix value)
                     :exec value))
         (strength (mbe :logic (nfix strength)
                        :exec strength)))
      (std::prod-cons value strength))))