MetricSpaces Andrew Sneap {-# OPTIONS --safe --without-K #-} module MetricSpaces.index where import MetricSpaces.DedekindReals import MetricSpaces.Rationals import MetricSpaces.StandardDefinition -- by Tom de Jong import MetricSpaces.Type