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