Skip to content

Vector library needs to replaced/deprecated. #54

Open
rocq-prover/rocq
#16765
@ejgallego

Description

@ejgallego

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

No one assigned

    Labels

    No labels
    No labels

    Projects

    Status

    In progress

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions