		Search-engine friendly clone of the ACL2 documentation.

Fty-pseudo-term-utilities

Fty-check-fn-call

FTY version of check-fn-call.

Signature
(fty-check-fn-call term) → (mv yes/no fn args)
Arguments: term — Guard (pseudo-termp term).
Returns: yes/no — Type (booleanp yes/no).; fn — Type (symbolp fn).; args — Type (pseudo-term-listp args).

Definitions and Theorems

Function: fty-check-fn-call

(defun fty-check-fn-call (term)
  (declare (xargs :guard (pseudo-termp term)))
  (let ((__function__ 'fty-check-fn-call))
    (declare (ignorable __function__))
    (check-fn-call (pseudo-term-fix term))))

Theorem: booleanp-of-fty-check-fn-call.yes/no

(defthm booleanp-of-fty-check-fn-call.yes/no
  (b* (((mv ?yes/no ?fn acl2::?args)
        (fty-check-fn-call term)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: symbolp-of-fty-check-fn-call.fn

(defthm symbolp-of-fty-check-fn-call.fn
  (b* (((mv ?yes/no ?fn acl2::?args)
        (fty-check-fn-call term)))
    (symbolp fn))
  :rule-classes :rewrite)

Theorem: pseudo-term-listp-of-fty-check-fn-call.args

(defthm pseudo-term-listp-of-fty-check-fn-call.args
  (b* (((mv ?yes/no ?fn acl2::?args)
        (fty-check-fn-call term)))
    (pseudo-term-listp args))
  :rule-classes :rewrite)

Theorem: true-listp-of-fty-check-fn-call.args

(defthm true-listp-of-fty-check-fn-call.args
  (b* (((mv ?yes/no ?fn acl2::?args)
        (fty-check-fn-call term)))
    (true-listp args))
  :rule-classes :type-prescription)

Theorem: fty-check-fn-call-not-quote

(defthm fty-check-fn-call-not-quote
  (b* (((mv ?yes/no ?fn acl2::?args)
        (fty-check-fn-call term)))
    (not (equal fn 'quote))))

Theorem: pseudo-term-list-count-of-check-fn-call.args

(defthm pseudo-term-list-count-of-check-fn-call.args
  (implies (pseudo-termp term)
           (b* (((mv yes/no & args)
                 (check-fn-call term)))
             (implies yes/no
                      (< (pseudo-term-list-count args)
                         (pseudo-term-count term)))))
  :rule-classes :linear)

Theorem: pseudo-term-list-count-of-fty-check-fn-call.args

(defthm pseudo-term-list-count-of-fty-check-fn-call.args
  (b* (((mv ?yes/no ?fn acl2::?args)
        (fty-check-fn-call term)))
    (implies yes/no
             (< (pseudo-term-list-count args)
                (pseudo-term-count term))))
  :rule-classes :linear)