eql
Major Section: ACL2-BUILT-INS
General Forms: (remove1 x lst) (remove1 x lst :test 'eql) ; same as above (eql as equality test) (remove1 x lst :test 'eq) ; same, but eq is equality test (remove1 x lst :test 'equal) ; same, but equal is equality test
(Remove1 x lst) is equal to lst if x is not a member of lst,
else is the result of removing the first occurrences of x from lst.
The optional keyword, :TEST, has no effect logically, but provides the
test (default eql) used for comparing x with successive elements of
lst.
Also see remove.
The guard for a call of remove1 depends on the test. In all cases,
the second argument must satisfy 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 remove1 and
its variants:
(remove1-eq x lst)is equivalent to(remove1 x lst :test 'eq);
(remove1-equal x lst)is equivalent to(remove1 x lst :test 'equal).
In particular, reasoning about any of these primitives reduces to reasoning
about the function remove1-equal.
