diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-05 15:25:50 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:15 +0100 |
| commit | d95fd157ac6600f4784de44ef558c4880aed624b (patch) | |
| tree | 7d6cc3a7eed8270fe0cb88aa47b2599809d6885f | |
| parent | 5d32732cdf110e44a51cf6a23a8972f015e3fc88 (diff) | |
COMMENT: question
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 9e5f18f52..f69b40278 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1246,6 +1246,11 @@ same as proving: $(\haslengthA~(\Nil~A)~\nO)$ and $\forall a:A, \forall l:\ListA, (\haslengthA~l~(\length~l)) \ra (\haslengthA~(\cons~A~a~l)~(\nS~(\length~l)))$. +% QUESTION: Wouldn't something like: +% +% http://matej-kosik.github.io/www/doc/coq/notes/25__has_length.html +% +% be more comprehensible? One conceptually simple way to do that, following the basic scheme proposed by Martin-L\"of in his Intuitionistic Type Theory, is to |