From a388d599ba461cf35b40c3850d593f5e9bb71d3d Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Fri, 6 Nov 2015 16:58:44 +0100
Subject: CLEANUP: Existing example was removed.

We have expanded the example above.
For consistency reasons, it would make sense to do the same also for this example.
However, due to the size of the terms, it is hard to typeset it nicely.
I propose to remove it.
---
 doc/refman/RefMan-cic.tex | 10 ----------
 1 file changed, 10 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index d2bae76f61..87d6f1d28e 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1591,16 +1591,6 @@ $ \CI{(\cons~\nat)}{P}
   \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
-\CI{(\conshl~A)}{P} is defined as:\\ 
-$\forall a:A, \forall l:\ListA, \forall n:\nat, \forall
-h:(\haslengthA~l~n), (P~(\cons~A~a~l)~(\nS~n)~(\conshl~A~a~l~n~l))$.\\ 
-If $P$ does not depend on its third argument, we find the more natural
-expression:\\ 
-$\forall a:A, \forall l:\ListA, \forall n:\nat,
-(\haslengthA~l~n)\ra(P~(\cons~A~a~l)~(\nS~n))$.
-
 \paragraph{Typing rule.}
 
 Our very general destructor for inductive definition enjoys the
-- 
cgit v1.2.3