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(-)

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


From f25c1d252ad61b4dc4321e3a11f33b1e6d4e3dff Mon Sep 17 00:00:00 2001
From: Timothy Bourke
Date: Sun, 22 Jul 2018 07:43:32 +0200
Subject: Docs: minor typo in W-Ind relative to text

The rule uses s'_j, the text refers to s_j, the latter is simpler in the
absence of any other constraints.
---
 doc/sphinx/language/cic.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 9f932ae78f..b670305389 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -961,7 +961,7 @@ such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;…;I_k :∀ Γ_P ,A_k]`,
 .. inference:: W-Ind
 
    \WFE{Γ_P}
-   (E[Γ_P ] ⊢ A_j : s_j' )_{j=1… k}
+   (E[Γ_P ] ⊢ A_j : s_j )_{j=1… k}
    (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n}
    ------------------------------------------
    \WF{E;\ind{p}{Γ_I}{Γ_C}}{Γ}
-- 
cgit v1.2.3


From 80883ddf89949afa82081ba80ccb4934320e6ee3 Mon Sep 17 00:00:00 2001
From: Timothy Bourke
Date: Sun, 22 Jul 2018 10:56:23 +0200
Subject: Docs: minor typo in "Template Polymorphism"

---
 doc/sphinx/language/cic.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index b670305389..721dc80b18 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1019,7 +1019,7 @@ Template polymorphism
 +++++++++++++++++++++
 
 Inductive types declared in :math:`\Type` are polymorphic over their arguments
-in :math:`\Type`. If :math:`A` is an arity of some sort and math:`s` is a sort, we write :math:`A_{/s}`
+in :math:`\Type`. If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}`
 for the arity obtained from :math:`A` by replacing its sort with :math:`s`.
 Especially, if :math:`A` is well-typed in some global environment and local
 context, then :math:`A_{/s}` is typable by typability of all products in the
-- 
cgit v1.2.3