coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Andreas Abel <andreas.abel AT ifi.lmu.de>
To: Tie Cheng <chengtie AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] "match (Zpos p?=0%Z) with ..." given "p : positive"
Date: Thu, 17 Feb 2011 18:53:37 +0100

Have you tried

case_eq (Zpos p?=0%Z).

?
On 2/17/11 5:53 PM, Tie Cheng wrote:

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

--
Andreas Abel <>< Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel AT ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/

[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