diff options
author | 2015-11-05 16:01:00 +0100 | |
---|---|---|
committer | 2015-12-10 09:35:16 +0100 | |
commit | 435c8b0fdf3c01d2618d1ffbbfe2321250326420 (patch) | |
tree | 0be3e5fe809cf3c0f5a6bd9604ad21a4020a48db | |
parent | 42039fff68ea24ad3fff58d17d79195faa0ee3e7 (diff) |
COMMENT: question
-rw-r--r-- | doc/refman/RefMan-cic.tex | 18 |
1 files changed, 17 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 34f55fa00..148c4505c 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1306,7 +1306,23 @@ The \kw{in} part can be omitted if the result type does not depend on the arguments of $I$. Note that the arguments of $I$ corresponding to parameters \emph{must} be \verb!_!, because the result type is not generalized to -all possible values of the parameters. The other arguments of $I$ +all possible values of the parameters. +% QUESTION: The last sentence above does not seem to be accurate. +% +% Imagine: +% +% Definition foo (A:Type) (a:A) (l : list A) := +% match l return A with +% | nil => a +% | cons _ _ _ => a +% end. +% +% There, the term in the return-clause happily refer to the parameter of 'l' +% and Coq does not protest. +% +% So I am not sure if I really understand why parameters cannot be bound +% in as-clause. +The other arguments of $I$ (sometimes called indices in the litterature) have to be variables ($a$ above) and these variables can occur in $P$ and bound in it. The expression after \kw{in} |