• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
      • Fgl
      • Vl
        • Syntax
        • Loader
        • Warnings
        • Getting-started
        • Utilities
          • Name-database
          • Vl-gc
          • Symbol-list-names
          • Ints-from
          • Nats-from
          • Make-lookup-alist
          • Redundant-mergesort
          • Longest-common-prefix
          • Vl-remove-keys
          • Vl-plural-p
          • Vl-merge-contiguous-indices
          • Sum-nats
          • Vl-edition-p
          • Vl-maybe-integer-listp
          • Fast-memberp
          • Nat-listp
            • Nat-listp-basics
          • Max-nats
          • Longest-common-prefix-list
          • Character-list-listp
          • Vl-character-list-list-values-p
          • Remove-from-alist
          • Prefix-of-eachp
          • Vl-string-keys-p
          • Vl-maybe-nat-listp
          • Vl-string-list-values-p
          • String-list-listp
          • Vl-string-values-p
          • Explode-list
          • True-list-listp
          • Symbol-list-listp
          • All-have-len
          • Pos-listp
          • Min-nats
          • Debuggable-and
          • Vl-starname
          • Remove-equal-without-guard
          • String-fix
          • Anyp
          • Vl-maybe-string-list
          • Longer-than-p
          • Fast-alist-free-each-alist-val
          • Not*
          • Free-list-of-fast-alists
          • *nls*
        • Printer
        • Kit
        • Mlib
        • Transforms
      • X86isa
      • Svl
      • Rtl
    • Software-verification
    • Testing-utilities
    • Math
  • Utilities

Nat-listp

(nat-listp x) recognizes lists where every element satisfies natp.

Signature
(nat-listp x) → std::bool

This is an ordinary deflist. It is "loose" in that it does not care whether x is nil-terminated.

Definitions and Theorems

Function: nat-listp

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

Subtopics

Nat-listp-basics
Basic theorems about nat-listp, generated by deflist.