• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
        • Defun
        • Declare
        • System-utilities
        • Stobj
        • State
        • Mutual-recursion
        • Memoize
        • Mbe
        • Io
        • Defpkg
        • Apply$
        • Loop$
        • Programming-with-state
        • Arrays
        • Characters
        • Time$
        • Defmacro
        • Loop$-primer
        • Fast-alists
        • Defconst
        • Evaluation
        • Guard
        • Equality-variants
        • Compilation
        • Hons
        • ACL2-built-ins
        • Developers-guide
        • System-attachments
        • Advanced-features
        • Set-check-invariant-risk
        • Numbers
        • Efficiency
        • Irrelevant-formals
        • Introduction-to-programming-in-ACL2-for-those-who-know-lisp
        • Redefining-programs
        • Lists
          • Member
          • Append
          • List
          • Nth
          • Len
          • True-listp
          • String-listp
          • Nat-listp
          • Character-listp
          • Symbol-listp
          • True-list-listp
          • Length
          • Search
          • Intersection$
          • Union$
          • Remove-duplicates
          • Position
          • Update-nth
          • Take
          • Nthcdr
          • Set-difference$
          • Subsetp
          • No-duplicatesp
          • Concatenate
          • Remove
          • Remove1
          • Intersectp
          • Endp
          • Keyword-value-listp
          • Integer-listp
          • Reverse
          • Add-to-set
          • List-utilities
          • Set-size
          • Revappend
          • Subseq
          • Make-list
          • Last
          • Lists-light
          • Boolean-listp
          • Butlast
          • Pairlis$
          • Substitute
          • Count
            • Duplicity
          • Keyword-listp
          • List*
          • Eqlable-listp
          • Pos-listp
          • Integer-range-listp
          • Rational-listp
          • Evens
          • Atom-listp
          • ACL2-number-listp
          • Typed-list-utilities
          • Odds
          • List$
          • Listp
          • Standard-char-listp
          • Last-cdr
          • Pairlis
          • Proper-consp
          • Improper-consp
          • Pairlis-x2
          • Pairlis-x1
          • Merge-sort-lexorder
          • Fix-true-list
          • Real-listp
        • Invariant-risk
        • Errors
        • Defabbrev
        • Conses
        • Alists
        • Set-register-invariant-risk
        • Strings
        • Program-wrapper
        • Get-internal-time
        • Basics
        • Packages
        • Oracle-eval
        • Defmacro-untouchable
        • <<
        • Primitive
        • Revert-world
        • Unmemoize
        • Set-duplicate-keys-action
        • Symbols
        • Def-list-constructor
        • Easy-simplify-term
        • Defiteration
        • Fake-oracle-eval
        • Defopen
        • Sleep
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
      • Interfacing-tools
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Lists
  • Strings
  • ACL2-built-ins

Count

Count the number of occurrences of an item in a string or true-list

Example Forms:
(count #\D "DabcDefcDe")                 ; = 3
(count #\D "DabcDefcDe" :start 1)        ; = 2
(count #\D "DabcDefcDe" :start 1 :end 5) ; = 1
(count #\D "DabcDefcDe" :start 1 :end 4) ; = 0
(count #\z "DabcDefcDe")                 ; = 0
(count '(a b) '(17 (a b) 23 (a b) (c d)))   ; = 2

General Form:
(count item sequence &key start end)

(Count item sequence) returns the number of times item occurs in sequence. The guard for calls of count (which is actually a macro in ACL2) specifies that sequence is a string or a true-list, and that start, which defaults to 0, and end, which defaults to the length of sequence, are valid indices into sequence.

See any Common Lisp documentation for more information about count, which is a Common Lisp utility. At this time ACL2 does not support keyword arguments for count other than :start and :end; we may add support for the :from-end keyword upon request.

Macro: count

(defmacro count (item sequence &key (start '0) end)
  (cons 'count-fn
        (cons item
              (cons sequence
                    (cons start (cons end 'nil))))))

Subtopics

Duplicity
(duplicity a x) counts how many times the element a occurs within the list x.