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: Adam Chlipala <adam AT chlipala.net>
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 11:56:31 -0500

Tie Cheng wrote:

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?

I would expect [simpl] to do the job.

[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