Andrew Sneap \begin{code} {-# OPTIONS --safe --without-K #-} module MetricSpaces.index where import MetricSpaces.Alternative -- by Tom de Jong import MetricSpaces.Type import MetricSpaces.DedekindReals import MetricSpaces.Rationals \end{code}