Martin Escardo \begin{code} {-# OPTIONS --safe --without-K --exact-split #-} module CoNaturals.index where import CoNaturals.Arithmetic import CoNaturals.Exercise -- with Chuangjie Xu import CoNaturals.GenericConvergentSequence import CoNaturals.UniversalProperty \end{code}