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: Oct 13 2024 at 01:02 UTC