coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac extend

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Ltac extend
Date: Thu, 22 Sep 2016 09:03:34 +0000
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f182.google.com
Ironport-phdr: 9a23:gXBn0xCFtYTrQzwMK25/UyQJP3N1i/DPJgcQr6AfoPdwSP38psbcNUDSrc9gkEXOFd2CrakV0ayO7+u4CSRAuc/H6y9SNsQUFlcssoY/oU8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUt2as8Pi3OervpbXfg9ghTynYLo0Ig/lgx/Ws5w0iJBlLO4e0BzSuTMcee1NwmVnP1WIhEfU6cK5/Zol+CNV7aFyv/VcWLn3KvxrBYdTCy4rZjg4

Coq is always turning tactics into terms. The two examples in 8.4 are proof scripts ([Show Proof] will give you the term) and typeclass resolution. The ltac: scope, when used in the constr: scope, behaves the same way. (I hope it is documented, but I am not entirely sure.) It is a new feature of Coq 8.5. (The typeclass trick I suggested is a way of mimicking it while maintaining compatibility with 8.4. Tangentially, I would be curious to know if typeclasses are significantly different in efficiency from tactics in terms.)

On Thu, Sep 22, 2016, 1:55 AM Laurent Thery <Laurent.Thery AT inria.fr> wrote:

>> constr:(ltac:(first [is_var x; exact true|exact false])).

What I don't understand is how Coq turns a tactic into a term.
Is this constr:(ltac:_) documented in the manual or is this a feature?

--
Laurent

[Coq-Club] Ltac extend, Frédéric Besson, 09/20/2016
- Re: [Coq-Club] Ltac extend, Pierre-Marie Pédrot, 09/20/2016
  - Re: [Coq-Club] Ltac extend, Frédéric Besson, 09/21/2016
    - Re: [Coq-Club] Ltac extend, Jason Gross, 09/21/2016
      - Re: [Coq-Club] Ltac extend, Frédéric Besson, 09/22/2016
        
        Re: [Coq-Club] Ltac extend, Robbert Krebbers, 09/22/2016
        
        Re: [Coq-Club] Ltac extend, Frédéric Besson, 09/22/2016
        
        Re: [Coq-Club] Ltac extend, Laurent Thery, 09/22/2016
        Re: [Coq-Club] Ltac extend, Jason Gross, 09/22/2016
        
        Re: [Coq-Club] Ltac extend, Jonathan Leivent, 09/22/2016