coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert"

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert"
Date: Tue, 20 Jan 2015 11:58:08 +0000
Accept-language: de-DE, en-US

Dear Coq users,

Is there a tactic which remembers the value of a term (not just its type as assert does) but allows to supply the value using tactics rather than giving an explicit term? Something half way between set and assert.

Thanks & best regards,

Michael

[Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Soegtrop, Michael, 01/20/2015
- Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Arnaud Spiwack, 01/20/2015
  - RE: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Soegtrop, Michael, 01/20/2015
    - Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Pierre-Marie Pédrot, 01/20/2015
      - Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Arnaud Spiwack, 01/20/2015
        
        RE: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Georges Gonthier, 01/20/2015
        
        RE: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Soegtrop, Michael, 01/21/2015
        
        Re: [Coq-Club] Tactic which remebers the value like "set" but creates a goal like "assert", Enrico Tassi, 01/21/2015