On Tue, Dec 21, 2010 at 5:02 PM, Daniel Fischer <[email protected]> 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?
Even if the theorem does hold with infinite structures, I don't really know the answer to your question. I'm just starting to study Coq in my free time =). My guess would be "no", because functions need to be total. But that's just a wild guess, and you shouldn't take my word for it =). Cheers! -- Felipe. _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
