		Search-engine friendly clone of the ACL2 documentation.

Pnumber-number-nondigit

Make-pnumber-number-nondigit

Basic constructor macro for pnumber-number-nondigit structures.

Syntax

(make-pnumber-number-nondigit [:number <number>] 
                              [:nondigit <nondigit>])

This is the usual way to construct pnumber-number-nondigit structures. It simply conses together a structure with the specified fields.

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

Definition

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

Macro: make-pnumber-number-nondigit

(defmacro make-pnumber-number-nondigit (&rest args)
  (std::make-aggregate 'pnumber-number-nondigit
                       args '((:number) (:nondigit))
                       'make-pnumber-number-nondigit
                       nil))

Function: pnumber-number-nondigit

(defun pnumber-number-nondigit (number nondigit)
  (declare (xargs :guard (and (pnumberp number)
                              (characterp nondigit))))
  (declare (xargs :guard (str::letter/uscore-char-p nondigit)))
  (b* ((number (mbe :logic (pnumber-fix number)
                    :exec number))
       (nondigit (mbe :logic (acl2::char-fix nondigit)
                      :exec nondigit)))
    (let ((nondigit (mbe :logic
                         (if (str::letter/uscore-char-p nondigit)
                             nondigit
                           #\_)
                         :exec nondigit)))
      (cons :number-nondigit (list number nondigit)))))