mirror of
https://git8.cs.fau.de/theses/bsc-leon-vatthauer.git
synced 2024-05-31 07:28:34 +02:00
42 lines
1 KiB
Agda
42 lines
1 KiB
Agda
|
{-# OPTIONS --guardedness #-}
|
|||
|
|
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′
|
|||
|
|
|
|||
|
|
mutual
|
|||
|
|
repeat : {A : Set} (a : A) → coList A
|
|||
|
|
repeat′ : {A : Set} (a : A) → coList′ A
|
|||
|
|
repeat {A} a = a ∷ repeat′ a
|
|||
|
|
force (repeat′ {A} a) = repeat a
|