alternating_bools.agda

open import Data.Bool
open import Relation.Binary.PropositionalEquality renaming (refl to definition-chasing)

record List (A : Set) : Set where
  -- Explicitly coinductive.
  -- The fields of this record are the destructors of this coinductive type.
  -- Notice: /No/ cons!
  coinductive
  field
    car : A
    cdr : List A

-- This places ~car~ and ~cdr~ in scope.
open List

-- Define ~alternate~ by the List destructors with copatterns.
alternate : {A : Set} → A → A → List A
car (alternate a b) = a
cdr (alternate a b) = alternate b a

-- Does this actually work?
test₀ : car (alternate true false) ≡ true
test₀ = definition-chasing

test₁ : car (cdr (alternate true false)) ≡ false
test₁ = definition-chasing