coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs

From: Gregory Malecha <gmalecha AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs
Date: Mon, 7 Mar 2016 11:00:26 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-vk0-f52.google.com
Ironport-phdr: 9a23:vdW+lRISDfIuIDKNa9mcpTZWNBhigK39O0sv0rFitYgULf7xwZ3uMQTl6Ol3ixeRBMOAu60C27Od6vm9EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ35vxh7n5osSOKyxzxxODIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46Fp34d6XK77Z6U1S6BDRHRjajhtpZ6jiR6WZgyWrlAYT29exhFPGk3O6Azwdpb3qCrz8ORnjnq0J8rzGJ8uVDul9bYjbRbshSwHPnZt/2TejsF7jKtzrxeophg5yInRNtLGfMFid7/QKItJDVFKWdxcAmkYWtux

Thanks Jonathan --

Yes, this notation should be declared parsing only. You should make a similar notation without the tactics-in-terms to get nice printing.

On Sat, Mar 5, 2016 at 3:59 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 03/05/2016 06:53 PM, Ralf Jung wrote:

...The Notation you defined, is this useful for printing at all? I doubt the pretty printer can figure out if the actual proof term it sees, when it prints some @Var_ctx, was actually generated using the given tactic, so it could either ignore the ltac:(...) when printing, or it could just never use this notation for printing.

There are bugs (for example: https://coq.inria.fr/bugs/show_bug.cgi?id=4595) involved in attempting to print notations that involve tactic-in-term. It's probably best to declare them "only parsing".

-- Jonathan

gregory malecha

Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, (continued)
- Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Ralf Jung, 03/03/2016
- Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Robbert Krebbers, 03/03/2016
  - Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Robbert Krebbers, 03/03/2016
    - Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Clément Pit--Claudel, 03/03/2016
      - Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Ralf Jung, 03/04/2016
        
        Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Gregory Malecha, 03/05/2016
        
        Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Ralf Jung, 03/06/2016
        
        Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Jonathan Leivent, 03/06/2016
        Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Gregory Malecha, 03/07/2016