2
module FakeProjectionsDoNotPreserveGuardedness where
5
open import Common.Coinduction
12
_×_ : (A B : Set) → Set
13
_,_ : {A B : Set}(a : A)(b : B) → A × B
14
proj₁ : {A B : Set}(p : A × B) → A
15
proj₂ : {A B : Set}(p : A × B) → B
20
data Stream (A : Set) : Set where
21
_∷_ : (x : A) (xs : ∞ (Stream A)) → Stream A
25
repeat : {A : Set}(a : A) → Stream A
26
repeat a = a ∷ proj₂ (repeat' a)
28
repeat' : {A : Set}(a : A) → A × ∞ (Stream A)
29
repeat' a = a , ♯ repeat a