count the number of occurrences of an item in a string or true-list
Major Section:  ACL2-BUILT-INS

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.