From 6bce3de10ec1cd18c60e1ce3b5af33350ec4ac86 Mon Sep 17 00:00:00 2001
From: Timothy Bourke
Date: Sat, 21 Jul 2018 18:11:25 +0200
Subject: 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.
---
 doc/sphinx/language/cic.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc/sphinx')

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\\
-- 
cgit v1.2.3