Skip to content

Redundancies between realseq.v and sequences.v #255

@affeldt-aist

Description

@affeldt-aist

There are redundancies between altreals/realseq.v (which predates MathComp-Analysis) and the newer sequences.v. How should we factorize?

Related issue: "The merge of sequences and sums over general sets (see esum.v and realsum.v)" (copy-paste from the wiki)

Metadata

Metadata

Assignees

No one assigned

    Labels

    question ❓There is an unanswered question hererenaming/refactoring 🔧This is about a renaming or refactoring in the library

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions