coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>
- To: Woon Ming <woon_ming AT comp.nus.edu.sg>
- Cc: Coq Club <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] Occurrence of keyword in conclusion
- Date: Thu, 29 Jan 2009 16:22:13 +0100
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Le 30 janv. 09 à 05:01, Woon Ming a écrit :
Hi Matthieu,
Hi Woon,
Thank you very much for your prompt reply. I have seen that pattern
construction when I was reading the reference manual (under Chapter 9.1
Syntax). However, the reason why I didn't use it is because there is no
worked examples on it.
There's a little explanation and an example in the 9.2 "Semantics" section.
It is a variant of [match goal with] expression.
Thus may I ask you to give me a simple example on how it is done so that?
On your example, you could probably simply write
[match goal with context [keyword] => ... end]
Hope this helps,
-- Matthieu
- [Coq-Club] Occurrence of keyword in conclusion, Woon Ming
- Re: [Coq-Club] Occurrence of keyword in conclusion,
Matthieu Sozeau
- RE: [Coq-Club] Occurrence of keyword in conclusion,
Woon Ming
- Re: [Coq-Club] Occurrence of keyword in conclusion, Matthieu Sozeau
- RE: [Coq-Club] Occurrence of keyword in conclusion,
Woon Ming
- Re: [Coq-Club] Occurrence of keyword in conclusion,
Matthieu Sozeau
Archive powered by MhonArc 2.6.16.