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 14:13:24 +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 mga06.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.0.116
Ironport-phdr: 9a23:fO9OnxYT2tiQ8XWbJSGMzT7/LSx+4OfEezUN459isYplN5qZpsW7bnLW6fgltlLVR4KTs6sC0LWG9f24EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i76vnYuHUC1Pg1sY+/xB4T6jsKt1un09YeZK1FDgyP4ardvJj23qx/Qv48Ym90xBLw2z06DmXxFdPhMwnssbXeSlBb168P6tMpm8i9Qsv8lsdVHXKrmZaMgZb1eEDkidWsy4Zu45lH4UQKT6y5EAS0tmR1SDl2d4Q==

Dear Maxime,

having () [] and {} for explicit, implicit and maximally inserted implicit
parameters, and using this notation in the standard library instead of () and
directives, would indeed by a good option.

Can you explain why the parameter scope is different in the two definitions?

Best regards,

Michael

Michael Soegtrop
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