Andrew Sneap

\begin{code}

{-# OPTIONS --safe --without-K #-}

module DedekindReals.index where

import DedekindReals.Type
import DedekindReals.Addition
import DedekindReals.Extension
import DedekindReals.Functions
import DedekindReals.Multiplication
import DedekindReals.Order
import DedekindReals.Properties

\end{code}