AndrasKovacs

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

{-
Large countable ordinals in Agda. For examples, see the bottom of this file.
Checked with Agda 2.6.0.1.

Countable ordinals are useful in "big number" contests, because they
can be directly converted into fast-growing ℕ → ℕ functions via the
fast-growing hierarchy:

copumpkin

module Primes where

open import Level using (_⊔_)
open import Coinduction
open import Function
open import Data.Empty
open import Data.Unit
open import Data.Nat
open import Data.Nat.Properties
open import Data.Nat.Divisibility