Re: [Haskell-cafe] Proof in Haskell

...

...

...

...

"Daniel" == Daniel Fischer 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