Stream: Coq users

Topic: How to use some functions from Util.List?


view this post on Zulip Thomas Baruchel (Mar 07 2024 at 13:15):

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.

view this post on Zulip Kenji Maillard (Mar 07 2024 at 13:50):

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

view this post on Zulip Thomas Baruchel (Mar 07 2024 at 16:05):

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