From 435c8b0fdf3c01d2618d1ffbbfe2321250326420 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Thu, 5 Nov 2015 16:01:00 +0100 Subject: COMMENT: question --- doc/refman/RefMan-cic.tex | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) (limited to 'doc/refman') 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} -- cgit v1.2.3