coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Gyesik Lee" <gyesik.lee AT aist.go.jp>
- To: coq-club <coq-club AT pauillac.inria.fr>
- Subject: [Coq-Club] Question about the tactic simpl
- Date: Wed, 19 Nov 2008 20:59:52 +0900
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:sender:to:subject:mime-version:content-type :content-transfer-encoding:content-disposition:x-google-sender-auth; b=M9P4Yfy1vEiacoHu1IGiaI4/NOmnWk48MSyD4fGrkp1iHvMPjXD8K2PoS15HEPAX8W b73Ly8HRxwn29W66/n1k0P6W2K9uSuSgoaMY1wHhgD6VJTtqGX6NVV2CUKaxPc07Im/5 BbvErgBhoYJFI/rbcC8Kn2QaJ4BUK6BgKj+Z4=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
This time a technical question.
Assume something is defined by using Fixpoint.
But inside the definition there is another recursive function is used.
During a proof, when I use the tactic "simpl", then every thing will
be so to speak decompressed.
Can I have, however, that just the outermost recursive cases get expanded?
One could use the tactic "change" to bring back the other espansions.
But it is a more work. So....
- [Coq-Club] Question about the tactic simpl, Gyesik Lee
- Re: [Coq-Club] Question about the tactic simpl, Adam Chlipala
Archive powered by MhonArc 2.6.16.