From 754bc95497ccf903391e5aa1cfda45cb59ad7927 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Tue, 3 Nov 2015 10:23:19 +0100
Subject: ENH: new example: "even"

---
 doc/common/macros.tex     |  5 +++++
 doc/refman/RefMan-cic.tex | 36 ++++++++++++++++++++++++++++++++++++
 2 files changed, 41 insertions(+)

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 1ac29b1553..0ea2ed650b 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -280,6 +280,11 @@
 \newcommand{\Type}{\mbox{\textsf{Type}}}
 \newcommand{\unfold}{\mbox{\textsf{unfold}}}
 \newcommand{\zeros}{\mbox{\textsf{zeros}}}
+\newcommand{\even}{\mbox{\textsf{even}}}
+\newcommand{\odd}{\mbox{\textsf{even}}}
+\newcommand{\evenO}{\mbox{\textsf{even\_O}}}
+\newcommand{\evenS}{\mbox{\textsf{even\_S}}}
+\newcommand{\oddS}{\mbox{\textsf{odd\_S}}}
 
 %%%%%%%%%
 % Misc. %
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index bbf6372846..101c4e5036 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -640,6 +640,42 @@ and thus it enriches the global environment with the following entry:
 
 \vskip1em\hrule\vskip1em
 
+\noindent If we take the following inductive definition:
+\begin{coq_example*}
+Inductive even : nat -> Prop :=
+  | even_O : even 0
+  | even_S : forall n, odd n -> even (S n)
+with odd : nat -> Prop :=
+  | odd_S : forall n, even n -> odd (S n).
+\end{coq_example*}
+then:
+\def\GammaI{\left[\begin{array}{r \colon l}
+                    \even & \nat\ra\Prop \\
+                    \odd & \nat\ra\Prop
+                  \end{array}
+            \right]}
+\def\GammaC{\left[\begin{array}{r \colon l}
+                    \evenO & \even~\nO \\
+                    \evenS & \forall n : \nat, \odd~n \ra \even~(\nS~n)
+                  \end{array}
+            \right]}
+\begin{itemize}
+  \item $p = 1$
+  \item $\Gamma_I = \GammaI$
+  \item $\Gamma_C = \GammaC$
+\end{itemize}
+and thus it enriches the global environment with the following entry:
+\vskip.5em
+\ind{p}{\Gamma_I}{\Gamma_C}
+\vskip.5em
+\noindent that is:
+\vskip.5em
+\ind{1}{\GammaI}{\GammaC}
+\vskip.5em
+\noindent In this case, $\Gamma_P=[A:\Type]$.
+
+\vskip1em\hrule\vskip1em
+
 \noindent If we take the following inductive definition:
 \begin{coq_example*}
 Inductive has_length (A : Type) : list A -> nat -> Prop :=
-- 
cgit v1.2.3