		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-numrange-info

Make-deftreeops-numrange-info

Basic constructor macro for deftreeops-numrange-info structures.

Syntax

(make-deftreeops-numrange-info [:get-nat-fn <get-nat-fn>] 
                               [:bounds-thm <bounds-thm>])

This is the usual way to construct deftreeops-numrange-info structures. It simply conses together a structure with the specified fields.

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

Definition

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

Macro: make-deftreeops-numrange-info

(defmacro make-deftreeops-numrange-info (&rest args)
  (std::make-aggregate 'deftreeops-numrange-info
                       args '((:get-nat-fn) (:bounds-thm))
                       'make-deftreeops-numrange-info
                       nil))

Function: deftreeops-numrange-info

(defun deftreeops-numrange-info (get-nat-fn bounds-thm)
  (declare (xargs :guard (and (common-lisp::symbolp get-nat-fn)
                              (common-lisp::symbolp bounds-thm))))
  (declare (xargs :guard t))
  (let ((__function__ 'deftreeops-numrange-info))
    (declare (ignorable __function__))
    (b* ((get-nat-fn (mbe :logic (acl2::symbol-fix get-nat-fn)
                          :exec get-nat-fn))
         (bounds-thm (mbe :logic (acl2::symbol-fix bounds-thm)
                          :exec bounds-thm)))
      (list (cons 'get-nat-fn get-nat-fn)
            (cons 'bounds-thm bounds-thm)))))