diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-04-26 10:59:23 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-26 10:59:23 +0200 |
commit | 68b576a178c057a016c7d4be1b319cc8fcbfac25 (patch) | |
tree | 49559c5743db0cb642f761c0e618aa58d227997b /doc/sphinx/language | |
parent | 83c3ee8659f1cee68909570fbf581a0e03233af7 (diff) | |
parent | 31c04ca25cbb9963d74060746ba57460d98acbfe (diff) |
Merge PR #7181: Sphinx docs: clarify strict implicit arguments a bit
Diffstat (limited to 'doc/sphinx/language')
-rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 1a7628d89..3f4fbbd6f 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -1436,7 +1436,9 @@ For instance, the first argument of in module ``List.v`` is strict because :g:`list` is an inductive type and :g:`A` will always be inferable from the type :g:`list A` of the third argument of -:g:`cons`. On the contrary, the second argument of a term of type +:g:`cons`. Also, the first argument of :g:`cons` is strict with respect to the second one, +since the first argument is exactly the type of the second argument. +On the contrary, the second argument of a term of type :: forall P:nat->Prop, forall n:nat, P n -> ex nat P |