coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] more naive questions about rewriting

From: "John Wiegley" <johnw AT newartisans.com>
To: Vadim Zaliva <vzaliva AT cmu.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] more naive questions about rewriting
Date: Tue, 16 Aug 2016 17:06:30 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jwiegley AT gmail.com; spf=Pass smtp.mailfrom=jwiegley AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f182.google.com
Ironport-phdr: 9a23:RdC+mxwmv8uIiY7XCy+O+j09IxM/srCxBDY+r6Qd0eMUIJqq85mqBkHD//Il1AaPBtSCrasUwLGP++C4ACpbsM7H6ChDOLV3FDY9wf0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3CwN5K6zPF5LIiIzvjqbpqsSVOlUD32P1Iesrak7n9UOJ7oheqLAhA5558gHOrHpMdrYe7kJTDnXXoSzB4Nyt9oVo6SVatqFp3cdBVaLnY/ZwFuQAX3wOelo478zztBTFURDHpj5FCj1XwVJ0BF375R37W9/Duy/7qOM1jDeINMn3U7kcUjG/qapnVUm7pj0AMmtz0mbXjIRPja9UpB+w7VQrwYnUZp69Mvdhd7nBfMgTQ3EHVcFUAX8SSrigZpcCWrJSdd1TqJPw8h5X9UOz
Organization: New Artisans LLC

>>>>> "VZ" == Vadim Zaliva
>>>>> <vzaliva AT cmu.edu>
>>>>> writes:

VZ> Of course I can try to use 'remember' to give them shorter names, but that
VZ> would require copy-pasting them into 'remember' statement.

remember does accept wildcards:

remember (f _ _ _ _ _ _ _) as F.

--
John Wiegley GPG fingerprint = 4710 CF98 AF9B 327B B80F
http://newartisans.com 60E1 46C4 BD1A 7AC1 4BA2

[Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/16/2016
- Re: [Coq-Club] more naive questions about rewriting, Laurent Thery, 08/16/2016
  - Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/17/2016
    - Re: [Coq-Club] more naive questions about rewriting, John Wiegley, 08/17/2016
    - Re: [Coq-Club] more naive questions about rewriting, Laurent Thery, 08/17/2016
  - Re: [Coq-Club] more naive questions about rewriting, Jonathan Leivent, 08/17/2016
    - Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/17/2016
      - Re: [Coq-Club] more naive questions about rewriting, Matthieu Sozeau, 08/17/2016
        
        Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/18/2016
        
        Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/18/2016
        
        Re: [Coq-Club] more naive questions about rewriting, Matthieu Sozeau, 08/18/2016
        Re: [Coq-Club] more naive questions about rewriting, Vadim Zaliva, 08/19/2016