Martin Escardo and Paulo Oliva 2011

\begin{code}

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

module InfinitePigeon.DataStructures where

\end{code}

Some definitions of standard things
(sorry for not using libraries).

\begin{code}

open import InfinitePigeon.Addition
open import InfinitePigeon.Finite
open import InfinitePigeon.LogicalFacts
open import InfinitePigeon.Naturals

data List (X : Set) : Set where
 [] : List X
 _::_  : X → List X → List X

infixr  _::_

\end{code}

Transforms a finite list given as a map to an enumerated finite
list:

\begin{code}

list : {m : ℕ} {X : Set} → (smaller m → X) → List X
list {} s = []
list {succ m} s = s fzero :: list {m} (s ∘ fsucc)

\end{code}

Binary products:

\begin{code}

data _×_ (X Y : Set) : Set where
 _,_ : X → Y → X × Y

infixr  _,_

\end{code}

The cons operation for the Cantor space:

\begin{code}

open import InfinitePigeon.Cantor
open import InfinitePigeon.Two

_^_ : ℕ → ₂ℕ → ₂ℕ
(O ^ α) O = ₀
(O ^ α) (succ i) = α i
(succ n ^ α) O = ₁
(succ n ^ α) (succ i) = α i

infixr  _^_

\end{code}

Take a finite initial sublist of an infinite sequence.

\begin{code}

take : (m : ℕ) {X : Set} → (ℕ → X) → List X
take  α = []
take (succ m) α = α  :: take m (α ∘ succ)

\end{code}

Index a finite sequence:

\begin{code}

_!_ : {m : ℕ} → (smaller(m + ) → ℕ) → ℕ → ℕ
_!_ {m} s n = s(fmin m n)

\end{code}