[Haskell-cafe] Proof in Haskell

[Colin Paul Adams]

>>>>> "Daniel" == Daniel Fischer <daniel.is.fischer at googlemail.com> 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