Docs: Fix p values in CIC Inductive Defs examples

It seems that p is a natural number, so why not write it as 0 rather
than the empty list for tree and forest?

And, if I understand correctly, odd and even have p = 0 and
Arr(even) = Arr(odd) = 1.

1 files changed, 2 insertions, 2 deletions

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 98e81ebc65..9f932ae78f 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -745,7 +745,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is
    is:
 
    .. math::
-      \ind{~}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]}
+      \ind{0}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]}
        {\left[\begin{array}{rcl}
                 \node &:& \forest → \tree\\
                 \emptyf &:& \forest\\
@@ -766,7 +766,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is
    The declaration for a mutual inductive definition of even and odd is:
 
    .. math::
-      \ind{1}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\
+      \ind{0}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\
                                       \odd&:&\nat → \Prop \end{array}\right]}
        {\left[\begin{array}{rcl}
                 \evenO &:& \even~0\\