• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Hons-and-memoization
    • Events
    • History
    • Parallelism
    • Programming
    • Start-here
    • Real
    • Debugging
    • Miscellaneous
      • Term
        • Lambda
        • Pseudo-termp
        • Term-order
        • Pseudo-term-listp
        • Guard-holders
        • Termp
          • Logic-fns-list-listp
          • Logic-fnsp
          • Logic-fns-listp
          • Logic-termp
          • Logic-term-list-listp
          • Logic-term-listp
        • L<
        • Kwote
        • Kwote-lst
      • Ld
      • Hints
      • Type-set
      • Ordinals
      • ACL2-customization
      • With-prover-step-limit
      • With-prover-time-limit
      • Set-prover-step-limit
      • Local-incompatibility
      • Set-case-split-limitations
      • Subversive-recursions
      • Specious-simplification
      • Defsum
      • Oracle-timelimit
      • Thm
      • Defopener
      • Gcl
      • Case-split-limitations
      • Set-gc-strategy
      • Default-defun-mode
      • Top-level
      • Reader
      • Ttags-seen
      • Adviser
      • Ttree
      • Abort-soft
      • Defsums
      • Gc$
      • With-timeout
      • Coi-debug::fail
      • Expander
      • Gc-strategy
      • Coi-debug::assert
      • Sin-cos
      • Def::doc
      • Syntax
      • Subversive-inductions
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Termp
• ACL2-built-ins

Logic-fns-list-listp

Recognizer for when a given list of lists of terms calls only :logic-mode function symbols

For a list x of lists of terms in world wrld, (logic-fns-list-listp x wrld) is true if and only if every function symbol called in x is in :logic mode in wrld. Unlike logic-term-list-listp, logic-fns-list-listp does not check that x is a list of lists of terms; rather, logic-fns-list-listp should only be applied to such lists. See defun-mode-lambdas for some clarifications of how :program mode functions are allowed in certain :logic mode terms.

Function: logic-fns-list-listp

(defun logic-fns-list-listp (x wrld)
       (declare (xargs :guard (and (plist-worldp wrld)
                                   (pseudo-term-list-listp x))))
       (cond ((endp x) t)
             (t (and (logic-fns-listp (car x) wrld)
                     (logic-fns-list-listp (cdr x) wrld)))))