coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Edsko de Vries <Edsko.de.Vries AT cs.tcd.ie>
- To: Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] moving around let ... in
- Date: Mon, 9 Feb 2009 13:19:18 +0000
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
You need to break 'n' down into its compontents:
On 9 Feb 2009, at 13:12, Keiko Nakata wrote:
Goal forall (f: nat -> nat) (n: nat * nat),Proof.
let (n1, _) := n in f n1 = f (let (n1, _) := n in n1).
intros.
destruct n.
reflexivity.
Qed.
- E
- [Coq-Club] moving around let ... in, Keiko Nakata
- Re: [Coq-Club] moving around let ... in, Edsko de Vries
- Re: [Coq-Club] moving around let ... in, Guillaume Melquiond
Archive powered by MhonArc 2.6.16.