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.
