From 56abd3ce281e3fd8f3df27597c6348d6ab033b64 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 6 Nov 2015 16:58:22 +0100
Subject: ENH: existing example was expanded

---
 doc/refman/RefMan-cic.tex | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 91c1418546..d2bae76f61 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1584,9 +1584,12 @@ branch corresponding to the $c:C$ constructor.
 We write \CI{c}{P} for \CI{c:C}{P} with $C$ the type of $c$.
 
 \paragraph{Examples.}
-For $\List \nat$ the type of $P$ will be $\ListA\ra s$ for $s \in \Sort$. \\ 
-$ \CI{(\cons~A)}{P} \equiv
-\forall a:A, \forall l:\ListA,(P~(\cons~A~a~l))$.
+For $\List~\nat$ the type of $P$ will be $\List~\nat\ra s$ for $s \in \Sort$. \\ 
+$ \CI{(\cons~\nat)}{P}
+  \equiv\CI{(\cons~\nat) : (\nat\ra\List~\nat\ra\List~\nat)}{P} \equiv\\
+  \equiv\forall n:\nat, \CI{(\cons~\nat~n) : \List~\nat\ra\List~\nat)}{P} \equiv\\
+  \equiv\forall n:\nat, \forall l:\List~\nat, \CI{(\cons~\nat~n~l) : \List~\nat)}{P} \equiv\\
+\equiv\forall n:\nat, \forall l:\List~\nat,(P~(\cons~\nat~n~l))$.
 
 For $\haslengthA$, the type of $P$ will be
 $\forall l:\ListA,\forall n:\nat, (\haslengthA~l~n)\ra \Prop$ and the expression
-- 
cgit v1.2.3