diff options
| author | Matej Kosik | 2015-11-04 18:54:17 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:14 +0100 |
| commit | 70e705a47f435e1453d889177a426d89dacda07b (patch) | |
| tree | 6159261534213be2342d8fdf06401278e793d124 | |
| parent | d0d4eb3aedc2d971a1ab4182ac5e4ee3ac741427 (diff) | |
COMMENT: question
| -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. |