diff options
Diffstat (limited to 'doc/faq/FAQ.tex')
| -rw-r--r-- | doc/faq/FAQ.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex index 48b61827d..213fb0313 100644 --- a/doc/faq/FAQ.tex +++ b/doc/faq/FAQ.tex @@ -2587,8 +2587,8 @@ It is the language of commands of Gallina i.e. definitions, lemmas, {\ldots} \Question{What is a dependent type?} -A dependant type is a type which depends on some term. For instance -``vector of size n'' is a dependant type representing all the vectors +A dependent type is a type which depends on some term. For instance +``vector of size n'' is a dependent type representing all the vectors of size $n$. Its type depends on $n$ \Question{What is a proof by reflection?} |