coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] minimal example for "tac; tac in H; tac in *"

From: t x <txrev319 AT gmail.com>
To: Jason Gross <jasongross9 AT gmail.com>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] minimal example for "tac; tac in H; tac in *"
Date: Thu, 15 Aug 2013 00:30:36 +0000

Exactly what I needed. Thanks!

Minimal example for anyone stumbling across this thread in the future.

Tactic Notation "mysimp" :=
idtac "mysimp no arguments".

Tactic Notation "mysimp" "in" ident(x) :=
idtac "mysimp called on" x.

Tactic Notation "mysimp" "in" "*" :=
idtac "mysimp called on *".

Lemma lem1:
forall x, x + 1 = x -> False.
Proof.
intros.
mysimp.
mysimp in H.
mysimp in *.

On Wed, Aug 14, 2013 at 4:38 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

You're looking for the "Tactic Notation" vernacular command.

-Jason

On Wednesday, August 14, 2013, t x wrote:

Hi,

Can someone point me at documentation / minimal example (or even the right keyword to google for this) for designing a Ltac

Ltac tac := ...

s.t.

"tac;" --> idtac "case 0"
"tac in H;" --> idtac H;
"tac in *;" --> idtac "all"

Thanks!

[Coq-Club] minimal example for "tac; tac in H; tac in *", t x, 08/14/2013
- Re: [Coq-Club] minimal example for "tac; tac in H; tac in *", Jason Gross, 08/14/2013
  - Re: [Coq-Club] minimal example for "tac; tac in H; tac in *", t x, 08/15/2013