Skip to Content.
Sympa Menu

coq-club - [Coq-Club] intro vs intros

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] intro vs intros


Chronological Thread 
  • 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





Archive powered by MHonArc 2.6.18.

Top of Page