DataStructures

Martin Escardo and Paulo Oliva 2011


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

module InfinitePigeon.DataStructures where


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


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

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

infixr  _::_


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


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


Binary products:


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

infixr  _,_


The cons operation for the Cantor space:


open import InfinitePigeon.Cantor
open import InfinitePigeon.Two

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

infixr  _^_


Take a finite initial sublist of an infinite sequence.


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


Index a finite sequence:


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