diff options
author | Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-03 10:37:16 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:12 +0100 |
commit | 6c9f5450f476da94aa70df93c5a6368b98e73e90 (patch) | |
tree | 418b4542787ee21b1599c56dc41827e544cc4ad5 /doc | |
parent | 754bc95497ccf903391e5aa1cfda45cb59ad7927 (diff) |
CLEANUP: superfluous examples were removed
Diffstat (limited to 'doc')
-rw-r--r-- | doc/common/macros.tex | 2 | ||||
-rw-r--r-- | doc/refman/RefMan-cic.tex | 20 |
2 files changed, 6 insertions, 16 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 0ea2ed650..a6240ad28 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -281,7 +281,7 @@ \newcommand{\unfold}{\mbox{\textsf{unfold}}} \newcommand{\zeros}{\mbox{\textsf{zeros}}} \newcommand{\even}{\mbox{\textsf{even}}} -\newcommand{\odd}{\mbox{\textsf{even}}} +\newcommand{\odd}{\mbox{\textsf{odd}}} \newcommand{\evenO}{\mbox{\textsf{even\_O}}} \newcommand{\evenS}{\mbox{\textsf{even\_S}}} \newcommand{\oddS}{\mbox{\textsf{odd\_S}}} diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 101c4e503..d3e8755a8 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -763,21 +763,11 @@ 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\ra\Type\\ - \prefix\Nil : \forall~A\!:\!\Type,~\List~A\\ - \prefix\cons : \forall~A\!:\!\Type,~A\ra\List~A\ra\List~A\\ - \prefix\haslength : \forall~A\!:\!\Type,~\List~A\ra\nat\ra\Prop\\ - \prefix\nilhl : \forall~A\!:\!\Type,~\haslength~A~(\Nil~A)~\nO\\ - \begin{array}{l l} - \hskip-.5em\prefix\conshl :\hskip-.5em & \forall~A\!:\!\Type,~\forall~a\!:\!A,~\forall~l\!:\!\List~A,~\forall~n\!:\!\nat,\\ - & \haslength~A~l~n\ra \haslength~A~(\cons~A~a~l)~(\nS~n) - \end{array} + \prefix\even : \nat\ra\Prop\\ + \prefix\odd : \nat\ra\Prop\\ + \prefix\evenO : \even~\nO\\ + \prefix\evenS : \forall~n:\nat, \odd~n \ra \even~(\nS~n)\\ + \prefix\oddS : \forall~n:\nat, \even~n \ra \odd~(\nS~n) \end{array}$ %\paragraph{Parameters.} |