Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] about Tactic Notation: a variant of apply ... with ...

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] about Tactic Notation: a variant of apply ... with ...


chronological Thread 
  • From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
  • To: AUGER Cédric <Cedric.Auger AT lri.fr>
  • Cc: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] about Tactic Notation: a variant of apply ... with ...
  • Date: Wed, 21 Jul 2010 10:45:16 +0900
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:cc:content-type :content-transfer-encoding; b=BuiTTBf5WOBweue/gfjdYwv2Hk6KK6l/7t2yuumemLrR0+9/uWzhqF6uvR/7ExRPwQ EAW6Z96kM2owY+2XqmJAdP+qdfSR4KGjeR7jydGBb0u9Wl7vrfoLrKw2HMlqhIskCKaA FjnfT0BWyEQe7BNs5MSIDcODUvMqhYmKVRPlA=
Hi,

> That is not very satisfying, but isn't it possible to do something like:
>
> Tactic Notation "sapply" constr(H) "with" ?a :=
> simpl; apply Â H with ?a.
>
> Tactic Notation "sapply" constr(H) "with" ?a ?b :=
> simpl; apply Â H with ?a ?b.
>
> Tactic Notation "sapply" constr(H) "with" ?a ?b ?c :=
> simpl; apply Â H with ?a ?b ?c.
>
> Tactic Notation "sapply" constr(H) "with" ?a ?b ?c ?d :=
> simpl; apply Â H with ?a ?b ?c ?d.
>
> Tactic Notation "sapply" constr(H) "with" ?a ?b ?c ?d ?e :=
> simpl; apply Â H with ?a ?b ?c ?d ?e.
>
> So that you can use list of at most 5 parameters.
> I know it shouldn't be the right way to do this, but also consider that
> having a list of more than 6 terms could mean that a dedicated tactic
> is welcome.

many thanks for the suggestion. It provides a reasonable solution to
my problems.

Gyesik


Archive powered by MhonArc 2.6.16.

Top of Page