[Haskell-cafe] Proof in Haskell

Daniel Fischer daniel.is.fischer at googlemail.com
Tue Dec 21 20:02:15 CET 2010

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.

Since mirror (mirror x) = x doesn't hold in Haskell, I take it that Coq 
doesn't allow infinite structures?

More information about the Haskell-Cafe mailing list