On Tuesday 21 December 2010 20:11:37, Colin Paul Adams wrote: > >>>>> "Daniel" == Daniel Fischer <[email protected]> > >>>>> 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. _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
