Computable analysis and notions of continuity in Coq

Florian Steinberg, Laurent Thery, Holger Thies

We give a number of formal proofs of theorems from the field of computable analysis. Many of our results specify executable algorithms that work on infinite inputs by means of oper…