• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • C
      • Soft
      • Bv
      • Imp-language
      • Ethereum
      • Event-macros
      • Java
      • Riscv
      • Bitcoin
      • Zcash
      • Yul
        • Transformations
          • Renaming-variables
          • Dead-code-eliminator
          • Renamings
          • Disambiguator
          • Unique-variables
          • Dead-code-eliminator-static-safety
          • No-function-definitions
            • Statements/blocks/cases/fundefs-nofunp
            • No-function-definitions-in-dynamic-semantics
            • Fundef-list-nofunp
              • Fundef-list-nofunp-basics
            • Statements-to-fundefs-when-nofunp
          • Unique-functions
          • Renaming-functions
          • Dead-code-eliminator-no-loop-initializers
          • Dead-code-eliminator-no-function-definitions
          • No-loop-initializers
          • For-loop-init-rewriter
        • Language
        • Yul-json
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Axe
      • Lists-light
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• No-function-definitions

Fundef-list-nofunp

Check that a list of function definitions has no nested function definitions.

Signature

(fundef-list-nofunp x) → std::bool

This lifts fundef-nofunp to lists. Analogously to fundef-nofunp, the function definitions passed as argument to fundef-list-nofunp are okay, but we check that they do not contain function definitions.

Definitions and Theorems

Function: fundef-list-nofunp

(defun fundef-list-nofunp (x)
  (declare (xargs :guard (fundef-listp x)))
  (let ((__function__ 'fundef-list-nofunp))
    (declare (ignorable __function__))
    (if (consp x)
        (and (fundef-nofunp (car x))
             (fundef-list-nofunp (cdr x)))
      t)))

Theorem: fundef-list-nofunp-of-fundef-list-fix-x

(defthm fundef-list-nofunp-of-fundef-list-fix-x
  (equal (fundef-list-nofunp (fundef-list-fix x))
         (fundef-list-nofunp x)))

Theorem: fundef-list-nofunp-fundef-list-equiv-congruence-on-x

(defthm fundef-list-nofunp-fundef-list-equiv-congruence-on-x
  (implies (fundef-list-equiv x x-equiv)
           (equal (fundef-list-nofunp x)
                  (fundef-list-nofunp x-equiv)))
  :rule-classes :congruence)

Subtopics

Fundef-list-nofunp-basics

Basic theorems about fundef-list-nofunp, generated by std::deflist.