`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`

.