Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.)


Chronological Thread 
  • From: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Prop smuggling (was: Re: Smart case analysis in Coq.)
  • Date: Thu, 24 Jul 2014 16:28:26 +0200

Try this in trunk. It will hopefully explain better than words:

Goal exists n, n=0.
Proof.
  refine (ex_intro _ _ _).

Currently the only way to introduce dependent subgoal is to use the [refine] tactic.


On 24 July 2014 15:05, Jonathan <jonikelee AT gmail.com> wrote:
On 07/24/2014 05:27 AM, Arnaud Spiwack wrote:
... the new dependent subgoal feature

What is the new dependent subgoal feature?

-- Jonathan







Archive powered by MHonArc 2.6.18.

Top of Page