diff options
| author | Matej Kosik | 2015-11-02 15:31:56 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:11 +0100 |
| commit | 089f2195aa0d0351b5692a8b4c947c7652d148b0 (patch) | |
| tree | 518bf97eac32caf29eb54d698cc6efd845ba027e | |
| parent | 42bc6762952b2d4996e26285720b3e556a63c96d (diff) | |
SILENT: s/coq_example/coq_example*/
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 2eb79ce842..574ef33c2d 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -535,11 +535,11 @@ $\forall\Gamma_P, T^\prime$. \subsection*{Examples} If we take the following inductive definition (denoted in concrete syntax): -\begin{coq_example} +\begin{coq_example*} Inductive bool : Set := | true : bool | false : bool. -\end{coq_example} +\end{coq_example*} then: \def\colon{@{\hskip.5em:\hskip.5em}} \def\GammaI{\left[\begin{array}{r \colon l} @@ -575,11 +575,11 @@ and thus it enriches the global environment with the following entry: \vskip1em\hrule\vskip1em \noindent If we take the followig inductive definition: -\begin{coq_example} +\begin{coq_example*} Inductive nat : Set := | O : nat | S : nat -> nat. -\end{coq_example} +\end{coq_example*} then: \def\GammaI{\left[\begin{array}{r \colon l} \nat & \Set @@ -608,11 +608,11 @@ 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} +\begin{coq_example*} Inductive list (A : Type) : Type := | nil : list A | cons : A -> list A -> list A. -\end{coq_example} +\end{coq_example*} then: \def\GammaI{\left[\begin{array}{r \colon l} \List & \Type\rightarrow\Type @@ -641,12 +641,12 @@ 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} +\begin{coq_example*} Inductive Length (A : Type) : list A -> nat -> Prop := | Lnil : Length A (nil A) O | Lcons : forall (a:A) (l:list A) (n:nat), Length A l n -> Length A (cons A a l) (S n). -\end{coq_example} +\end{coq_example*} then: \def\GammaI{\left[\begin{array}{r \colon l} \Length & \forall~A\!:\!\Type,~\List~A\rightarrow\nat\rightarrow\Prop @@ -676,13 +676,13 @@ 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} +\begin{coq_example*} Inductive tree : Set := | node : forest -> tree with forest : Set := | emptyf : forest | consf : tree -> forest -> forest. -\end{coq_example} +\end{coq_example*} then: \def\GammaI{\left[\begin{array}{r \colon l} \tree & \Set\\ |