Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Bind argument of tactic notation to scope

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Bind argument of tactic notation to scope


Chronological Thread 
  • From: Ralf Jung <jung AT mpi-sws.org>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Bind argument of tactic notation to scope
  • Date: Sat, 20 Feb 2016 21:41:21 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
  • Ironport-phdr: 9a23:V6KLzRVA3fpeOJukrgFQzVmWBR/V8LGtZVwlr6E/grcLSJyIuqrYZheGt8tkgFKBZ4jH8fUM07OQ6PC/HzFaqs/a7TgrS99laVwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oM2MJVgSz2PmPPtbF1afk0b4joEum4xsK6I8mFPig0BjXKBo/15uPk+ZhB3m5829r9ZJ+iVUvO89pYYbCf2pN/dwcbsNBzM/dmsx+cfDtB/ZTALJ6GFPfH8Rl09yCgzLpDPnWJi55innsOVV3TGbeNbpVvYzQzv0vPQjcwPhlCpSb21xy2rQkMEl1K8=

Hi all,

Is it somehow possible to bind the argument of a tactic notation to a
scope? I would like something similar to what we can do with

Arguments... _%S.

for functions and with

Notation "{[ e ]}" := (f e%S).

for normal notation. I tried this:

Tactic Notation "assume" constr(P) := cut (P%S).

but it does not seem to have any effect. See the attached file for an
example.

Kind regards,
Ralf
Delimit Scope my_scope with M.
Notation "P ★ Q" := (P /\ Q) (at level 20) : my_scope.

Tactic Notation "assume" constr(P) := cut (P%M).

Goal True.
(* Would like to bind the argument of the assume tactic to my_scope:
   assume (True ★ False). *)
assume (True ★ False).



Archive powered by MHonArc 2.6.18.

Top of Page