diff options
| author | Matej Kosik | 2015-11-02 16:15:38 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:11 +0100 |
| commit | 42347ebd180f10b738f628bae904b5773a0150ac (patch) | |
| tree | b8f965d0478acc2d3b9b38e9f347fe86ef155258 /doc | |
| parent | bc78fc26204d638f789597e2892d95483918f187 (diff) | |
COMMENT: to do
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index cc69355d4a..8f03cafd14 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -760,7 +760,9 @@ $\begin{array}{@{} l} \subsection{Well-formed inductive definitions} We cannot accept any inductive declaration because some of them lead -to inconsistent systems. We restrict ourselves to definitions which +to inconsistent systems. +% TODO: The statement above deserves explanation. +We restrict ourselves to definitions which satisfy a syntactic criterion of positivity. Before giving the formal rules, we need a few definitions: |