bsc-leon-vatthauer/thesis/agda/Coind.agda

{-# OPTIONS --guardedness #-}

-- Agda code that is included in the thesis.
-- just for making sure that everything used in the thesis actually compiles ;)

open import Agda.Builtin.Equality
module Coind where
module Streams where
  record Stream (A : Set) : Set where
    coinductive
    field
      head : A
      tail : Stream A
  open Stream

  repeat : {A : Set} (a : A) → Stream A
  head (repeat a) = a
  tail (repeat a) = repeat a

  record _≈_ {A} (s : Stream A) (t : Stream A) : Set where
    coinductive
    field
      head : head s ≡ head t
      tail : tail s ≈ tail t
  open _≈_

  repeat-eq : ∀ {A} (a : A) → repeat a ≈ tail (repeat a)
  head (repeat-eq {A} a) = refl
  tail (repeat-eq {A} a) = repeat-eq a

module coLists where
  mutual
    data coList (A : Set) : Set where
      nil : coList A
      _∷_ : A → coList′ A → coList A
    
    record coList′ (A : Set) : Set where
      coinductive
      field force : coList A
  open coList′

  module repeatMutual where 
    mutual
      repeat  : {A : Set} (a : A) → coList A
      repeat′ : {A : Set} (a : A) → coList′ A
      repeat a = a ∷ repeat′ a
      force (repeat′ a) = repeat a
  
  repeat : {A : Set} (a : A) → coList A
  repeat a = a ∷ λ { .force → repeat a }