		Search-engine friendly clone of the ACL2 documentation.

Deffixequiv-sk-implementation

Deffixequiv-sk-hints

Generate the hints for deffixequiv.

Signature
(deffixequiv-sk-hints fn fn-rule fn-witness bvars args-alist wrld) → hints
Arguments: fn — Guard (symbolp fn).; fn-rule — Guard (symbolp fn-rule).; fn-witness — Guard (symbolp fn-witness).; bvars — Guard (symbol-listp bvars).; args-alist — Guard (acl2::symbol-symbol-alistp args-alist).; wrld — Guard (plist-worldp wrld).
Returns: hints — Type (true-listp hints).

The hints consist of a :use hints with the lemma instances for all the arguments and an :in-theory hints to enable fn and disable fn-rule.

Definitions and Theorems

Function: deffixequiv-sk-hints

(defun deffixequiv-sk-hints (fn fn-rule
                                fn-witness bvars args-alist wrld)
 (declare (xargs :guard (and (symbolp fn)
                             (symbolp fn-rule)
                             (symbolp fn-witness)
                             (symbol-listp bvars)
                             (acl2::symbol-symbol-alistp args-alist)
                             (plist-worldp wrld))))
 (declare (xargs :guard (not (eq fn-witness 'quote))))
 (let ((__function__ 'deffixequiv-sk-hints))
  (declare (ignorable __function__))
  (b* ((args-names (strip-cars args-alist)))
   (cons
    (cons
      '"Goal"
      (cons ':in-theory
            (cons (cons 'e/d
                        (cons (cons fn 'nil)
                              (cons (cons fn-rule 'nil) 'nil)))
                  (cons ':use
                        (cons (deffixequiv-sk-lemma-insts-args
                                   fn-rule fn-witness
                                   bvars args-names args-alist wrld)
                              'nil)))))
    'nil))))

Theorem: true-listp-of-deffixequiv-sk-hints

(defthm true-listp-of-deffixequiv-sk-hints
  (b*
   ((hints (deffixequiv-sk-hints fn fn-rule
                                 fn-witness bvars args-alist wrld)))
   (true-listp hints))
  :rule-classes :rewrite)