		Search-engine friendly clone of the ACL2 documentation.

Sandwich

Make-sandwich

Basic constructor macro for sandwich structures.

Syntax

(make-sandwich [:bread <bread>] 
               [:fillings <fillings>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-sandwich

(defmacro make-sandwich (&rest args)
  (std::make-aggregate 'sandwich
                       args '((:bread) (:fillings))
                       'make-sandwich
                       nil))

Function: sandwich

(defun sandwich (bread fillings)
  (declare (xargs :guard (and (integerp bread)
                              (symbolp fillings))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'sandwich))
    (declare (ignorable acl2::__function__))
    (b* ((bread (mbe :logic (ifix bread) :exec bread))
         (fillings (mbe :logic (symbol-fix fillings)
                        :exec fillings)))
      (list (cons 'bread bread)
            (cons 'fillings fillings)))))