cau_seq, cauchy_seq

Stream: maths

[Yury G. Kudryashov]

Hi, what is the reason to introduce cau_seq in mathlib? When I first tried to understand what happens, presence of both cau_seq and cauchy_seq was really confusing. I can see that it makes some definitions computable but I don't think that cau_seq lead to any reasonable computable definitions. I mean, a computable Cauchy sequence without a computable estimate on the rate of convergence gives no information about the limit.

[Mario Carneiro]

It is a bootstrapping thing. cau_seq does not rely on any topology for its definition, but it is superceded by cauchy_seq