This is an archived version pinned as of the submission of my master's thesis. An up-to-date version may be found online.

Real numbers

Files in the real numbers folder

module real-numbers where

open import real-numbers.dedekind-real-numbers public
open import real-numbers.rational-real-numbers public