Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?


Chronological Thread 
  • From: Daniel Schepler <dschepler AT gmail.com>
  • To: coq-club AT inria.fr
  • Cc: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
  • Subject: Re: [Coq-Club] [coqdev] Tactic for detecting that there is a goal left?
  • Date: Wed, 18 Jun 2014 08:31:38 -0700

On Wednesday, June 18, 2014 02:10:36 PM Arnaud Spiwack wrote:
> is that t;[t1|…|tn] is *not* of the form t;t'. It is easily witnessed in
> that t;([t1|…|tn]) is not parsable. I could fix the problem by introducing
> a syntax [t1|…|tn] and make it so that ; [ is parsed specially and that we
> have to write t;([t1|…|tn]) to the the simple semantics. But I fear the
> complaints would be loud.

What if [t1|...|tn] meant: fail if the number of focused goals is not a
multiple of n; and if it is a multiple of n, apply t1, ..., tn round robin to
the focused goals.
--
Daniel Schepler




Archive powered by MHonArc 2.6.18.

Top of Page