Redundancies between `realseq.v` and `sequences.v`

Open affeldt-aist opened this issue 5 years ago • 3 comments

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)

Sep 04 '20 10:09 affeldt-aist

We can work on this together if you want.

Sep 08 '20 09:09 strub

:+1:

Sep 08 '20 09:09 CohenCyril