coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] match goal with context

From: Michael Shulman <mshulman AT ucsd.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] match goal with context
Date: Fri, 22 Apr 2011 12:48:26 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=f8GchE2kjGI4oBQpJeZ/zCxThhFFz9B2ktKMcUamuntx/7sajNimiUOjE9vTEJ2Rve b2uaiMXIYkmyrX9csP5d7dhiuq94wA0g/2AKoXO1HDFwrBRYKptaZzD5KlNmZN/8WjgY k/qIX7p7W45LtdD9jl0/YpObu93eZleap2bQE=

Hi everyone,

Is it possible to write a tactic which matches a subterm of the goal
against a pattern, i.e. to combine "match goal with" and the pattern
"context ident [cpattern]"?  The reference manual section "Pattern
matching on goals" says "Note also that matching against subterms
(using the context ident [ cpattern ]) is available and may itself
induce extra backtrackings," but the following tactic definition:

Ltac test :=
  match goal with
    context cxt [S ?X] => idtac X
  end.

produces the error message "Syntax error: ':' or ':=' expected after
[Prim.name] (in [match_hyps])."

Thanks!
Mike

[Coq-Club] match goal with context, Michael Shulman
- Re: [Coq-Club] match goal with context, Adam Chlipala