The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,

I don't think targetting beginners is a better choice than targetting experts in this problem. We should try to make switching between the two "modes" easier.

 

I guess a carefully written file (one per main sub-libraries?) containing a bunch of "Arguments .." commands should allow that.

My two cents,

Pierre

2017-09-14 18:27 GMT+02:00 Soegtrop, Michael <michael.soegtrop AT intel.com>:

Dear Coq Team,

> First command of the file: Set Implicit Arguments.

IMHO it is not a good idea to use this directive in the standard library. The standard library should be optimized for readability / understandability of individual definitions also by novice users and not for short writing.

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