CLEANUP: Presentation of examples was changed to make them more comprehensible.

1 files changed, 21 insertions, 6 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 574ef33c2d..cc69355d4a 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -722,12 +722,27 @@ contains an inductive declaration.
 \end{description}
 
 \paragraph{Example.}
-We have $(\List:\Set \ra \Set), (\cons:\forall~A:\Set,A\ra(\List~A)\ra
-(\List~A))$, \\ 
-$(\Length:\forall~A:\Set, (\List~A)\ra\nat\ra\Prop)$, $\tree:\Set$ and $\forest:\Set$.
-
-From now on, we write $\ListA$ instead of $(\List~A)$ and $\LengthA$
-for $(\Length~A)$.
+Provided that our environment $E$ contains inductive definitions we showed before,
+these two inference rules above enable us to conclude that:
+\vskip.5em
+\def\prefix{E[\Gamma]\vdash\hskip.25em}
+$\begin{array}{@{} l}
+   \prefix\bool : \Set\\
+   \prefix\true : \bool\\
+   \prefix\false : \bool\\
+   \prefix\nat : \Set\\
+   \prefix\nO : \nat\\
+   \prefix\nS : \nat\ra\nat\\
+   \prefix\List : \Type\rightarrow\Type\\
+   \prefix\Nil : \forall~A\!:\!\Type,~\List~A\\
+   \prefix\cons : \forall~A\!:\!\Type,~A\rightarrow\List~A\rightarrow\List~A\\
+   \prefix\Length : \forall~A\!:\!\Type,~\List~A\rightarrow\nat\rightarrow\Prop\\
+   \prefix\LNil : \forall~A\!:\!\Type,~\Length~A~(\Nil~A)~\nO\\
+   \begin{array}{l l}
+   \hskip-.5em\prefix\LCons :\hskip-.5em & \forall~A\!:\!\Type,~\forall~a\!:\!A,~\forall~l\!:\!\List~A,~\forall~n\!:\!\nat,\\
+                            & \Length~A~l~n\rightarrow \Length~A~(\cons~A~a~l)~(\nS~n)
+   \end{array}
+ \end{array}$
 
 %\paragraph{Parameters.}
 %%The parameters introduce a distortion between the inside specification