Tom de Jong, 10 March 2020

As suggested by Martin Escardo.

Cluster module for inductively defined dyadic rationals.

\begin{code}

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

module DyadicsInductive.index where

import DyadicsInductive.Dyadics
import DyadicsInductive.DyadicOrder
import DyadicsInductive.DyadicOrder-PropTrunc

\end{code}