Description
The Vector
and Fin
libraries are notoriously hard to use, and in some cases even impossible, (try rev (rev x) = x
)
See the thread at https://sympa.inria.fr/sympa/arc/coq-club/2017-12/msg00074.html for some discussion.
IMHO, these libraries are a source of pain for many new users and give a bad image of the stdlib, so Coq should provide an alternate mechanism to work with sized lists.
Metadata
Metadata
Assignees
Labels
No labels
Projects
Status
In progress