diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 00ba0091ee..1013084702 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -969,6 +969,10 @@ the type $V$ satisfies the nested positivity condition for $X$ \end{latexonly} \paragraph{Correctness rules.} +% QUESTION: For a related problem, in case of global definitions +% and global assumptions, we used the term "well-formedness". +% Couldn't we continue to use the term also here? +% Does it make sense to use a different name, i.e. "correctness" in this case? We shall now describe the rules allowing the introduction of a new inductive definition. |