		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

Lambda-logic-fnsp

Check if a lambda expression is in logic mode, i.e. its body is in logic mode.

Signature
(lambda-logic-fnsp lambd wrld) → yes/no
Arguments: lambd — Guard (pseudo-lambdap lambd).; wrld — Guard (plist-worldp wrld).
Returns: yes/no — Type (booleanp yes/no).

The name of this function is consistent with the name of logic-fnsp in the ACL2 source code.

Definitions and Theorems

Function: lambda-logic-fnsp

(defun lambda-logic-fnsp (lambd wrld)
  (declare (xargs :guard (and (pseudo-lambdap lambd)
                              (plist-worldp wrld))))
  (let ((__function__ 'lambda-logic-fnsp))
    (declare (ignorable __function__))
    (logic-fnsp (lambda-body lambd) wrld)))

Theorem: booleanp-of-lambda-logic-fnsp

(defthm booleanp-of-lambda-logic-fnsp
  (b* ((yes/no (lambda-logic-fnsp lambd wrld)))
    (booleanp yes/no))
  :rule-classes :rewrite)