>>>>> "Daniel" == Daniel Fischer <[email protected]> writes:
Daniel> On Tuesday 21 December 2010 19:34:11, Felipe Almeida Lessa wrote:
>>
> Theorem mirror_mirror : forall A (x : Tree A), mirror (mirror x) = x.
>> induction x; simpl; auto. rewrite IHx1; rewrite IHx2; trivial.
>> Qed.
Daniel> Since mirror (mirror x) = x doesn't hold in Haskell, I take
Daniel> it that Coq doesn't allow infinite structures?
Why doesn't it hold?
--
Colin Adams
Preston Lancashire
() ascii ribbon campaign - against html e-mail
/\ www.asciiribbon.org - against proprietary attachments
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
