Andrew Sneap

\begin{code}

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

module MetricSpaces.index where

import MetricSpaces.DedekindReals
import MetricSpaces.Rationals
import MetricSpaces.StandardDefinition -- by Tom de Jong
import MetricSpaces.Type

\end{code}