coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is there a tactic to do this in a convenient way?

From: Laurent Thery <Laurent.Thery AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Is there a tactic to do this in a convenient way?
Date: Sat, 12 Nov 2016 18:27:06 +0100

On 11/12/2016 04:42 PM, Chris Dams wrote:

Dear all,

In a proof I have a long and complicated term (let us call it
long_and_complicated_term) that is of a type that is of the form A -> B
-> C where all of A, B, and C are also long and complicated.

with the standard tactic:

Goal forall A B C D, (A -> B -> C) -> D.
intros A B C D H.
refine (_ (H _ _)); try intro H1.

--
Laurent

[Coq-Club] Is there a tactic to do this in a convenient way?, Chris Dams, 11/12/2016
- Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Xavier Leroy, 11/12/2016
- Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Jonathan Leivent, 11/12/2016
  - Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Jonathan Leivent, 11/12/2016
- Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Gabriel Scherer, 11/12/2016
- Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Dominique Larchey-Wendling, 11/12/2016
- Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Laurent Thery, 11/12/2016
  - Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Gabriel Scherer, 11/12/2016
  - Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Chris Dams, 11/13/2016
- Re: [Coq-Club] Is there a tactic to do this in a convenient way?, Gaetan Gilbert, 11/12/2016