DyadicsInductive

Tom de Jong, 10 March 2020

As suggested by Martin Escardo.

Cluster module for inductively defined dyadic rationals.


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

module DyadicsInductive.index where

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