coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Easy question re: implicit parameters

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Easy question re: implicit parameters
Date: Fri, 15 Sep 2017 15:02:35 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga04.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.0.116
Ironport-phdr: 9a23:832qrRNV3pJiEv8Or0kl6mtUPXoX/o7sNwtQ0KIMzox0K/X6rarrMEGX3/hxlliBBdydsK0UzbeO+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6a8TWO6mtYERLmcAFxO+7dG4jIjs3x2fr4s8nYZBwNjz6ga5tzKg+3pEPfrJ9Fr5FlL/N78RzErWdSfPwSjUZpLlKakhK2rpO1/ZVj+ilU/ekm+sFcS6LiV6U+UbFcSj8hNjZmt4XQqRDfQF7XtTMnWWIMn08QDg==

Dear Guillaume,

> Is there a use for non-maximal implicit arguments outside of legacy code?
> If not,
> adding a new binder syntax is not worth it.

Except that it would make it easier to gradually move standard library code
towards using maximal implicit arguments.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Easy question re: implicit parameters, Kevin Sullivan, 09/14/2017
- Re: [Coq-Club] Easy question re: implicit parameters, Guillaume Melquiond, 09/14/2017
  - Re: [Coq-Club] Easy question re: implicit parameters, Kevin Sullivan, 09/14/2017
  - RE: [Coq-Club] Easy question re: implicit parameters, Soegtrop, Michael, 09/14/2017
    - Re: [Coq-Club] Easy question re: implicit parameters, Pierre Courtieu, 09/15/2017
      - RE: [Coq-Club] Easy question re: implicit parameters, Soegtrop, Michael, 09/15/2017
        
        Re: [Coq-Club] Easy question re: implicit parameters, Maxime Dénès, 09/15/2017
        
        Re: [Coq-Club] Easy question re: implicit parameters, Ralf Jung, 09/15/2017
        
        RE: [Coq-Club] Easy question re: implicit parameters, Soegtrop, Michael, 09/15/2017
        
        Re: [Coq-Club] Easy question re: implicit parameters, Guillaume Melquiond, 09/15/2017
        
        RE: [Coq-Club] Easy question re: implicit parameters, Soegtrop, Michael, 09/15/2017
        Re: [Coq-Club] Easy question re: implicit parameters, Guillaume Melquiond, 09/15/2017
        RE: [Coq-Club] Easy question re: implicit parameters, Soegtrop, Michael, 09/15/2017
        Re: [Coq-Club] Easy question re: implicit parameters, Guillaume Melquiond, 09/15/2017
        Re: [Coq-Club] Easy question re: implicit parameters, Guillaume Melquiond, 09/15/2017
        Re: [Coq-Club] Easy question re: implicit parameters, Jason Gross, 09/16/2017
        
        RE: [Coq-Club] Easy question re: implicit parameters, Soegtrop, Michael, 09/18/2017
        Re: [Coq-Club] Easy question re: implicit parameters, Guillaume Melquiond, 09/18/2017
        RE: [Coq-Club] Easy question re: implicit parameters, Soegtrop, Michael, 09/18/2017
        
        RE: [Coq-Club] Easy question re: implicit parameters, Soegtrop, Michael, 09/18/2017
        
        Re: [Coq-Club] Easy question re: implicit parameters, Ralf Jung, 09/16/2017