From 8c82657e7692049dde4a4c44a2ea53d0c4fa7cb5 Mon Sep 17 00:00:00 2001 From: Anton Trunov Date: Tue, 27 Nov 2018 12:17:47 +0100 Subject: Document parameter names whenever possible As suggested by @ggonthier [here](https://github.com/math-comp/math-comp/pull/249#pullrequestreview-177938295) > One of the design ideas for the `Arguments` command was that it would allow to centralise the documentation of the application of constants. In that spirit it would be in my opinion better to make as much use of this as possible, and to document the parameter names whenever possible, especially that of implicit parameters. and [here](https://github.com/math-comp/math-comp/pull/253#discussion_r237434163): > As a general rule, defined functional constants should have maximal prenex implicit arguments, as this facilitates their use as arguments to functionals, because this mimics the way function constants are treated in functional programming languages with Hindley-Milner type inference. Conversely, lemmas and theorems should have on-demand implicit arguments, possibly interspersed with explicit ones, as it's fairly common for other lemmas to have universally quantified premises; also, this makes it easier to specify such arguments with the apply: tactic. This policy may be amended for lemmas that are used as functional arguments, such as reflection or cancellation lemmas. Unfortunately there is currently no easy way to tell Coq to use different defaults for definitions and lemmas, so MathComp sticks to the on-demand default, as there are significantly more lemmas than definition, and use the Prenex Implicits to redress matters in bulk for definitions. However, this is not completely systematic, and is sometimes omitted for constants that are not used as functional arguments in the library, or inside the sections in which the definition occur, since such commands need to be repeated after the section is closed. Since Arguments commands should document the intended constant usage as best as possible, they should follow the implicits policy - even in cases such as this where the Prenex Implicits had been skipped. --- mathcomp/algebra/vector.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'mathcomp/algebra/vector.v') diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index aef9a9f..542f8ad 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.v @@ -245,7 +245,7 @@ Definition f2mx (f : 'Hom(aT, rT)) := let: Hom A := f in A. Canonical hom_subType := [newType for f2mx]. End Hom. -Arguments mx2vs _ _ _%N _%MS. +Arguments mx2vs {K vT m%N} A%MS. Prenex Implicits v2r r2v v2rK r2vK b2mx vs2mx vs2mxK f2mx. End InternalTheory. -- cgit v1.2.3