		Search-engine friendly clone of the ACL2 documentation.

Oct-integer-literal

Make-oct-integer-literal

Basic constructor macro for oct-integer-literal structures.

Syntax

(make-oct-integer-literal [:digits/uscores <digits/uscores>] 
                          [:prefix-upcase-p <prefix-upcase-p>] 
                          [:suffix? <suffix?>])

This is the usual way to construct oct-integer-literal structures. It simply conses together a structure with the specified fields.

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

Definition

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

Macro: make-oct-integer-literal

(defmacro make-oct-integer-literal (&rest args)
  (std::make-aggregate 'oct-integer-literal
                       args
                       '((:digits/uscores)
                         (:prefix-upcase-p)
                         (:suffix?))
                       'make-oct-integer-literal
                       nil))

Function: oct-integer-literal

(defun oct-integer-literal (digits/uscores prefix-upcase-p suffix?)
 (declare
      (xargs :guard (and (octdig/uscore-listp digits/uscores)
                         (booleanp prefix-upcase-p)
                         (optional-integer-type-suffix-p suffix?))))
 (declare (xargs :guard (octdig/uscore-list-wfp digits/uscores)))
 (let ((__function__ 'oct-integer-literal))
   (declare (ignorable __function__))
   (b*
    ((digits/uscores
          (mbe :logic (octdig/uscore-list-fix digits/uscores)
               :exec digits/uscores))
     (prefix-upcase-p (mbe :logic (acl2::bool-fix prefix-upcase-p)
                           :exec prefix-upcase-p))
     (suffix? (mbe :logic (optional-integer-type-suffix-fix suffix?)
                   :exec suffix?)))
    (let ((digits/uscores
               (mbe :logic
                    (if (octdig/uscore-list-wfp digits/uscores)
                        digits/uscores
                      (list (octdig/uscore-digit (char-code #\0))
                            (octdig/uscore-digit (char-code #\0))))
                    :exec digits/uscores)))
      (cons :oct-integer-lit (list digits/uscores
                                   prefix-upcase-p suffix?))))))