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