coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] How does the simpl. tactics behave?

From: Taral <taralx AT gmail.com>
To: Z <zell08v AT orange.fr>
Cc: Adam Chlipala <adam AT chlipala.net>, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] How does the simpl. tactics behave?
Date: Tue, 7 Sep 2010 11:17:51 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; b=RPI3I95QVV3RlLrzN6uDQ1+I0HHShcl01LNLpjd31ABpSHHlXcfV5u41ouaheIuChU j6yrNLOdq64vBBuQJZBd/7QWZTUfXvuw5blK9aHnRlgX8Kj/UsXw0es+0fZVEX3MCRMo 2ZOYQ0uL/TLeIay34qUp8HcIMvXfuNLRHUPQo=

On Tue, Sep 7, 2010 at 9:43 AM, Z
<zell08v AT orange.fr>
wrote:
> *****************
> Definition gxx(x: nat) := match x with |_ =>0 end.
> Theorem test000bis: gxx 0 = 0.
> Proof. unfold gxx. Qed.
> *******************

If you want to understand better, try this:

Definition gxx(x: nat) := match x with |_ =>0 end.
Theorem test000bis: gxx 0 = 0.
Proof.
Print Proof.
unfold gxx.
Print Proof.
reflexivity.
Print Proof.
Qed.

--
Taral
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
� � -- Unknown

[Coq-Club] How does the simpl. tactics behave?, Z
- Re: [Coq-Club] How does the simpl. tactics behave?, Adam Chlipala
  - Re: [Coq-Club] How does the simpl. tactics behave?, Z
    - Re: [Coq-Club] How does the simpl. tactics behave?, Christine Paulin
      - Message not available
        
        Re: [Coq-Club] How does the simpl. tactics behave?, Z
        
        Re: [Coq-Club] How does the simpl. tactics behave?, Adam Chlipala
        
        Re: [Coq-Club] How does the simpl. tactics behave?, Z
        Re: [Coq-Club] How does the simpl. tactics behave?, Adam Chlipala
        
        Re: [Coq-Club] How does the simpl. tactics behave?, Taral
    - Re: [Coq-Club] How does the simpl. tactics behave?, Adam Chlipala