coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs
Date: Sat, 5 Mar 2016 18:59:45 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f175.google.com
Ironport-phdr: 9a23:GANM6RcB7e78a1cyp5ZrLV14lGMj4u6mDksu8pMizoh2WeGdxc6/YR7h7PlgxGXEQZ/co6odzbGG7Oa/CSdZvcfJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuMM04R2Gv1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu3MVv9nFvkAUHxmbjh0t4XXskzIShLK7X8BWE0XlABJCk7L9kLURJD05wn9sONh2CCcden7TK45Xyjqu6VsTh7rhSMKOhY29WjWjop7i6cN80HpnAB234OBONLdD/F5ZK6IIIsX

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

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