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

math-comp / analysis

Mathematical Components compliant Analysis Library

Other

203 stars 45 forks source link

Open affeldt-aist opened 4 years ago

affeldt-aist commented 4 years ago

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)

strub commented 4 years ago

We can work on this together if you want.

CohenCyril commented 4 years ago

:+1: