diff options
| -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 9e5f18f52a..f69b402783 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 |