[Haskell-cafe] Proof in Haskell

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

I wrote:

> 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?

Oops, mirroring infinite binary trees should work. Ignore above.

More information about the Haskell-Cafe mailing list