[Agda] Infinite proofs

[Yasuyuki Ogawa]

I've solved my 1 week trouble. Thank you all!

(2013/04/20 20:49), Altenkirch Thorsten wrote:
> On 20/04/2013 11:23, "Yasuyuki Ogawa" <lost_dog at nifty.com> wrote:
>
>> 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))
>
> You shouldn't use \sharp in the definition of a relation because it
> creates a new object each time you write \sharp. Instead you should use
> \flat in the definition of this relation - see Data/Stream in the library
> where this is defined as \approx.
>
>>
>> theorem-ones-eq' : StreamEq ones ones'
>> theorem-ones-eq' = ?
>
> Btw, the extensional equality on streams (\approx) *should* be the
> propositional equality. However, in the moment you can only achieve this
> by adding some postulates to Agda.
>
>
> Thorsten
>