POSITION

position of an item in a string or a list, using eql as test
Major Section:  PROGRAMMING

(Position item seq) is the least index (zero-based) of the element item in the string or list seq, if in fact item is an element of seq. Otherwise (position item seq) is nil.

(Position item lst) is provably the same in the ACL2 logic as (position-equal item lst). It has a stronger guard than position-equal because uses eql to test equality of item with members of lst. Its guard requires that either lst is a string, or else lst is a true list such that either (eqlablep item) or all members of lst are eqlablep. See position-equal and see position-eq.

Position is a Common Lisp function. See any Common Lisp documentation for more information. Since ACL2 functions cannot take keyword arguments (though macros can), the ACL2 functions position-equal and position-eq are defined to correspond to calls of the Common Lisp function position whose keyword argument :test is equal or eq, respectively.