1
{-# OPTIONS --copatterns #-}
7
record Tree (A : Set) : Set where
10
child : Bool -> Tree A
13
alternate : {A : Set}(a b : A) -> Tree A
14
label (child (alternate a b) false) = b
15
child (child (alternate a b) false) true = alternate a b
16
child (child (alternate a b) false) false = alternate a b
17
child {A = A} (alternate a b) true = alternate b a
18
label {A = A} (alternate a b) = a
20
{- Delivers an infinite tree
31
data List (A : Set) : Set where
33
_::_ : A -> List A -> List A
35
collect : List Bool -> {A : Set} -> Tree A -> List A
37
collect (b :: l) t = label t :: collect l (child t b)
40
test = collect (true :: true :: true :: []) (alternate true false)
b'\\ No newline at end of file'