coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive"

From: Tie Cheng <chengtie AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive"
Date: Thu, 17 Feb 2011 17:53:12 +0100
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:date:message-id:subject:from:to:content-type; b=Dp4QOZoIMd8MbCYaZtemEFPDQvijYcZG7nd5cAlxN8JEY5DcSVkXa30IpFTmMWQliF 5+U63nz/VgecmwqJsTjPXTdXtl/mzFi/vzmxMhEP+F/5hhEPb1TfYXN4rXd7RhAVi7wo uWXXKnlgcNTxtFSCv8ZXTSPth2R8E1TjVboTA=

Hello all,

I have "p : positive" in hypothsis and "match (Zpos p?=0%Z) with | Eq => ... | Gt => ... | Lt => ..." as part of the goal. Is there a tactic to remove the "match" from the goal?

Thanks and regards

Tie

[Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive", Tie Cheng
- Re: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive", Adam Chlipala
  - Re: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive", Tie Cheng
    - Re: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive", Adam Chlipala
      - Re: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive", Tie Cheng
- Re: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive", Andreas Abel