21 Dec
2010
21 Dec
'10
2:06 p.m.
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.