Skip to content

Redundancies between realseq.v and sequences.v #255

Open
Open
Redundancies between realseq.v and sequences.v#255
Labels
question ❓There is an unanswered question hererenaming/refactoring 🔧This is about a renaming or refactoring in the library
Milestone
1.19.0

Description

@affeldt-aist
affeldt-aist
opened on Sep 4, 2020

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)

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

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