[Haskell-cafe] Proof in Haskell
daniel.is.fischer at googlemail.com
Tue Dec 21 20:32:09 CET 2010
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
> > 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.
More information about the Haskell-Cafe