		Search-engine friendly clone of the ACL2 documentation.

Hint-pair

Make-hint-pair

Basic constructor macro for hint-pair structures.

Syntax

(make-hint-pair [:thm <thm>] 
                [:hints <hints>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-hint-pair

(defmacro make-hint-pair (&rest args)
  (std::make-aggregate 'hint-pair
                       args '((:thm) (:hints))
                       'make-hint-pair
                       nil))

Function: hint-pair

(defun hint-pair (thm hints)
  (declare (xargs :guard (and (pseudo-termp thm)
                              (true-listp hints))))
  (declare (xargs :guard t))
  (let ((acl2::__function__ 'hint-pair))
    (declare (ignorable acl2::__function__))
    (b* ((thm (mbe :logic (pseudo-term-fix thm)
                   :exec thm))
         (hints (mbe :logic (true-list-fix hints)
                     :exec hints)))
      (list (cons 'thm thm)
            (cons 'hints hints)))))