With `Require Import List.`

I can use some common functions, but I can see other ones at https://coq.inria.fr/doc/V8.19.1/api/coq-core/Util/List/index.html without managing to use them. Here is an example of session with an error:

```
Welcome to Coq 8.19.1
Require Import List.
Import ListNotations.
Compute last [2;3;4].
= fun _ : nat => 4
: nat -> nat
Compute distinct [2;3;4].
Toplevel input, characters 8-16:
> Compute distinct [2;3;4].
> ^^^^^^^^
Error: The reference distinct was not found in the current environment.
```

I am interested by functions like `eq_set`

or `subset`

.

The link you gave is the listing of functions available in order to implement coq (in ocaml), not the functions available in Coq to manipulate lists. You should have a look at the documentation of the Coq standard library https://coq.inria.fr/doc/V8.19.0/stdlib/Coq.Lists.List.html

Thank you, I understand better. I was aware of your own link, but I thought that I had found some separate collection of utilities. Regards.

Last updated: Jun 23 2024 at 03:02 UTC