diff options
| -rw-r--r-- | doc/sphinx/language/cic.rst | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 25a230015c..6ddfe14eea 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -930,7 +930,6 @@ condition* for a constant :math:`X` in the following cases: Inductive nattree (A:Type) : Type := | leaf : nattree A | node : A -> (nat -> nattree A) -> nattree A. - End TreeExample. Then every instantiated constructor of ``nattree A`` satisfies the nested positivity condition for ``nattree``: |