1
{-# OPTIONS --copatterns #-}
2
module CopatternNonterminating where
4
open import Common.Equality
6
record Stream (A : Set) : Set where
13
illdefined : {A : Set} -> Stream A
14
S.head illdefined = S.head illdefined
15
S.tail illdefined = S.tail illdefined
18
illRepeat : {A : Set}(a : A) → Stream A
19
( (S.head (illRepeat a))) = a
20
(S.head (S.tail (illRepeat a))) = a
21
(S.tail (S.tail (illRepeat a))) = S.tail (S.tail (illRepeat a))
25
illRepeat : {A : Set}(a : A) → Stream A
26
( (S.head (illRepeat a))) = a
27
(S.head (S.tail (illRepeat a))) = a
28
(S.tail (S.tail (illRepeat a))) = (S.tail (illRepeat a))
30
record _≈_ {A : Set}(s t : Stream A) : Set where
32
head : S.head s ≡ S.head t
33
tail : S.tail s ≈ S.tail t
36
repeat : {A : Set}(a : A) → Stream A
38
S.tail (repeat a) = repeat a
40
repeat′ : {A : Set}(a : A) → Stream A
41
( (S.head (repeat′ a))) = a
42
(S.head (S.tail (repeat′ a))) = a
43
(S.tail (S.tail (repeat′ a))) = S.tail (repeat′ a) -- invalid projection
45
repeat≈repeat′ : {A : Set}(a : A) → repeat a ≈ repeat′ a
46
( (B.head (repeat≈repeat′ a))) = refl
47
(B.head (B.tail (repeat≈repeat′ a))) = refl
48
(B.tail (B.tail (repeat≈repeat′ a))) = repeat≈repeat′ a