package alt-ergo-lib

If xs is empty, then uncons xs is None.

If xs is nonempty, then uncons xs is Some (x, ys) where x is the head of the sequence and ys its tail.

• since OCaml 4.14

is_empty xs determines whether the sequence xs is empty.

It is recommended that the sequence xs be persistent. Indeed, is_empty xs demands the head of the sequence xs, so, if xs is ephemeral, it may be the case that xs cannot be used any more after this call has taken place.

• since OCaml 4.14

append xs ys is the concatenation of the sequences xs and ys.

Its elements are the elements of xs, followed by the elements of ys.

• since OCaml 4.11

Provided the function eq defines an equality on elements, equal eq xs ys determines whether the sequences xs and ys are pointwise equal.

At least one of the sequences xs and ys must be finite.

• since OCaml 4.14