Skip to main content
PRL Project

next up previous
Next: Real Analysis in Up: Formalizing Constructive Real Analysis Previous: Formalizing Constructive Real Analysis


The first part of this paper is a guided tour through the real library with emphasis on the definitions, a handful of useful theorems, and the proof of the intermediate value theorem. Afterwards is a section giving detailed descriptions of the special-purpose tactics that were written in conjunction with the rationals and the reals. Users interested in developing theories in analysis should find both sections helpful.