[Agda] Infinite proofs

Yasuyuki Ogawa lost_dog at nifty.com
Sat Apr 20 12:23:53 CEST 2013

 > The usual solution is to define a custom equivalence relation 

Although I tried following code (is used in CPDT), I couldn't.
Is there something wrong?

data StreamEq {A : Set} : Stream A -> Stream A -> Set where
   streamEq : forall {a xs ys} -> StreamEq xs ys
     -> StreamEq (cons a (# xs)) (cons a (# ys))

theorem-ones-eq' : StreamEq ones ones'
theorem-ones-eq' = ?

More information about the Agda mailing list