		Search-engine friendly clone of the ACL2 documentation.

Support

Logic-mode-p

(logic-mode-p fn world) looks up the function fn and returns t if fn is in logic mode, or nil otherwise. It causes a hard error if fn isn't a function.

Definitions and Theorems

Function: logic-mode-p

(defun logic-mode-p (fn world)
  (declare (xargs :guard (and (symbolp fn)
                              (plist-worldp world))))
  (b* ((__function__ 'logic-mode-p)
       (look (getprop fn 'acl2::formals
                      :bad 'acl2::current-acl2-world
                      world))
       ((when (eq look :bad))
        (raise "Can't look up the formals for ~x0!"
               fn))
       (symbol-class (getprop fn 'acl2::symbol-class
                              nil 'acl2::current-acl2-world
                              world))
       ((unless (member symbol-class
                        '(:common-lisp-compliant :ideal :program)))
        (raise "Unexpected symbol-class for ~x0: ~x1."
               fn symbol-class)))
    (not (eq symbol-class :program))))

Theorem: booleanp-of-look-up-formals

(defthm booleanp-of-look-up-formals
  (or (equal (logic-mode-p fn world) t)
      (equal (logic-mode-p fn world) nil))
  :rule-classes :type-prescription)