coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Frederic Chyzak <frederic.chyzak AT inria.fr>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] intro vs intros
- Date: Sat, 13 Dec 2014 14:00:45 +0100
Hi,
I'm a newbie who has just taken his first lesson of (plain) Coq, now
trying his very first (plain) Coq exercises.
Many times, I find myself starting with some "intro x.", before
realizing I need to introduce another hypothesis, thus typing " y".
But, then, "intro x y." is an error, and I need to add an "s", to write
"intros x y.".
Is there a use case that motivates having two different tactic names?
Why not just make them absolute synonyms?
The problem is that I would like to use the same name, irrespective of
the number of arguments, and for that I would prefer typing the shorter
"intro".
Frédéric
- [Coq-Club] intro vs intros, Frederic Chyzak, 12/13/2014
- Re: [Coq-Club] intro vs intros, Arnaud Spiwack, 12/15/2014
Archive powered by MHonArc 2.6.18.