[Haskell-cafe] Proof in Haskell

[Daniel Fischer]

On Tuesday 21 December 2010 20:11:37, Colin Paul Adams wrote:
> >>>>> "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?

Hit send before I finished thinking, it should hold.