Major Section: ACL2-BUILT-INS
General Forms: (position x seq) (position x seq :test 'eql) ; same as above (eql as equality test) (position x seq :test 'eq) ; same, but eq is equality test (position x seq :test 'equal) ; same, but equal is equality test
(Position x seq) is the least index (zero-based) of the element x in
the string or list seq, if x is an element of seq. Otherwise
(position x seq) is nil. The optional keyword, :TEST, has no
effect logically, but provides the test (default eql) used for
comparing x with items of seq.
The guard for a call of position depends on the test. In all cases,
the second argument must satisfy stringp or true-listp. If the
test is eql, then either the first argument must be suitable for
eql (see eqlablep) or the second argument must satisfy
eqlable-listp. If the test is eq, then either the first argument
must be a symbol or the second argument must satisfy symbol-listp.
See equality-variants for a discussion of the relation between position and
its variants:
(position-eq x seq)is equivalent to(position x seq :test 'eq);
(position-equal x seq)is equivalent to(position x seq :test 'equal).
In particular, reasoning about any of these primitives reduces to reasoning
about the function position-equal.
Position is defined by Common Lisp. See any Common Lisp documentation for
more information.
