← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to doc/RecTutorial/coqartmacros.tex

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/RecTutorial/coqartmacros.tex
 
1
\usepackage{url}
 
2
 
 
3
\newcommand{\variantspringer}[1]{#1}
 
4
\newcommand{\marginok}[1]{\marginpar{\raggedright OK:#1}}
 
5
\newcommand{\tab}{{\null\hskip1cm}}
 
6
\newcommand{\Ltac}{\mbox{\emph{$\cal L$}tac}}
 
7
\newcommand{\coq}{\mbox{\emph{Coq}}}
 
8
\newcommand{\lcf}{\mbox{\emph{LCF}}}
 
9
\newcommand{\hol}{\mbox{\emph{HOL}}}
 
10
\newcommand{\pvs}{\mbox{\emph{PVS}}}
 
11
\newcommand{\isabelle}{\mbox{\emph{Isabelle}}}
 
12
\newcommand{\prolog}{\mbox{\emph{Prolog}}}
 
13
\newcommand{\goalbar}{\tt{}============================\it}
 
14
\newcommand{\gallina}{\mbox{\emph{Gallina}}}
 
15
\newcommand{\joker}{\texttt{\_}}
 
16
\newcommand{\eprime}{\(\e^{\prime}\)}
 
17
\newcommand{\Ztype}{\citecoq{Z}}
 
18
\newcommand{\propsort}{\citecoq{Prop}}
 
19
\newcommand{\setsort}{\citecoq{Set}}
 
20
\newcommand{\typesort}{\citecoq{Type}}
 
21
\newcommand{\ocaml}{\mbox{\emph{OCAML}}}
 
22
\newcommand{\haskell}{\mbox{\emph{Haskell}}}
 
23
\newcommand{\why}{\mbox{\emph{Why}}}
 
24
\newcommand{\Pascal}{\mbox{\emph{Pascal}}}
 
25
 
 
26
\newcommand{\ml}{\mbox{\emph{ML}}}
 
27
 
 
28
\newcommand{\scheme}{\mbox{\emph{Scheme}}}
 
29
\newcommand{\lisp}{\mbox{\emph{Lisp}}}
 
30
 
 
31
\newcommand{\implarrow}{\mbox{$\Rightarrow$}}
 
32
\newcommand{\metavar}[1]{?#1}
 
33
\newcommand{\notincoq}[1]{#1}
 
34
\newcommand{\coqscope}[1]{\%#1}
 
35
\newcommand{\arrow}{\mbox{$\rightarrow$}}
 
36
\newcommand{\fleche}{\arrow}
 
37
\newcommand{\funarrow}{\mbox{$\Rightarrow$}}
 
38
\newcommand{\ltacarrow}{\funarrow}
 
39
\newcommand{\coqand}{\mbox{\(\wedge\)}}
 
40
\newcommand{\coqor}{\mbox{\(\vee\)}}
 
41
\newcommand{\coqnot}{\mbox{\(\neg\)}}
 
42
\newcommand{\hide}[1]{}
 
43
\newcommand{\hidedots}[1]{...}
 
44
\newcommand{\sig}[3]{\texttt{\{}#1\texttt{:}#2 \texttt{|} #3\texttt{\}}}
 
45
\renewcommand{\neg}{\sim}
 
46
\renewcommand{\marginpar}[1]{}
 
47
 
 
48
\addtocounter{secnumdepth}{1}
 
49
\providecommand{\og}{�}
 
50
\providecommand{\fg}{�}
 
51
 
 
52
 
 
53
\newcommand{\hard}{\mbox{\small *}}
 
54
\newcommand{\xhard}{\mbox{\small **}}
 
55
\newcommand{\xxhard}{\mbox{\small ***}}
 
56
 
 
57
%%% Operateurs, etc.
 
58
\newcommand{\impl}{\mbox{$\rightarrow$}}
 
59
\newcommand{\appli}[2]{\mbox{\tt{#1 #2}}}
 
60
\newcommand{\applis}[1]{\mbox{\texttt{#1}}}
 
61
\newcommand{\abst}[3]{\mbox{\tt{fun #1:#2 \funarrow #3}}}
 
62
\newcommand{\coqle}{\mbox{$\leq$}}
 
63
\newcommand{\coqge}{\mbox{$\geq$}}
 
64
\newcommand{\coqdiff}{\mbox{$\neq$}}
 
65
\newcommand{\coqiff}{\mbox{$\leftrightarrow$}}
 
66
\newcommand{\prodsym}{\mbox{\(\forall\,\)}}
 
67
\newcommand{\exsym}{\mbox{\(\exists\,\)}}
 
68
 
 
69
\newcommand{\substsign}{/}
 
70
\newcommand{\subst}[3]{\mbox{#1\{#2\substsign{}#3\}}}
 
71
\newcommand{\anoabst}[2]{\mbox{\tt[#1]#2}}
 
72
\newcommand{\letin}[3]{\mbox{\tt let #1:=#2 in #3}}
 
73
\newcommand{\prodep}[3]{\mbox{\tt \(\forall\,\)#1:#2,$\,$#3}}
 
74
\newcommand{\prodplus}[2]{\mbox{\tt\(\forall\,\)$\,$#1,$\,$#2}}
 
75
\newcommand{\dom}[1]{\textrm{dom}(#1)} % domaine d'un contexte (log function)
 
76
\newcommand{\norm}[1]{\textrm{n}(#1)} % forme normale (log function)
 
77
\newcommand{\coqZ}[1]{\mbox{\tt{`#1`}}}
 
78
\newcommand{\coqnat}[1]{\mbox{\tt{#1}}}
 
79
\newcommand{\coqcart}[2]{\mbox{\tt{#1*#2}}}
 
80
\newcommand{\alphacong}{\mbox{$\,\cong_{\alpha}\,$}} % alpha-congruence
 
81
\newcommand{\betareduc}{\mbox{$\,\rightsquigarrow_{\!\beta}$}\,} % beta reduction
 
82
%\newcommand{\betastar}{\mbox{$\,\Rightarrow_{\!\beta}^{*}\,$}} % beta reduction
 
83
\newcommand{\deltareduc}{\mbox{$\,\rightsquigarrow_{\!\delta}$}\,} % delta reduction
 
84
\newcommand{\dbreduc}{\mbox{$\,\rightsquigarrow_{\!\delta\beta}$}\,} % delta,beta reduction
 
85
\newcommand{\ireduc}{\mbox{$\,\rightsquigarrow_{\!\iota}$}\,} % delta,beta reduction
 
86
 
 
87
 
 
88
% jugement de typage
 
89
\newcommand{\these}{\boldsymbol{\large \vdash}}
 
90
\newcommand{\disj}{\mbox{$\backslash/$}}
 
91
\newcommand{\conj}{\mbox{$/\backslash$}}
 
92
%\newcommand{\juge}[3]{\mbox{$#1 \boldsymbol{\vdash} #2 : #3 $}}
 
93
\newcommand{\juge}[4]{\mbox{$#1,#2 \these #3 \boldsymbol{:} #4 $}}
 
94
\newcommand{\smalljuge}[3]{\mbox{$#1 \these #2 \boldsymbol{:} #3 $}}
 
95
\newcommand{\goal}[3]{\mbox{$#1,#2 \these^{\!\!\!?} #3  $}}
 
96
\newcommand{\sgoal}[2]{\mbox{$#1\these^{\!\!\!\!?} #2 $}}
 
97
\newcommand{\reduc}[5]{\mbox{$#1,#2 \these #3 \rhd_{#4}#5 $}}
 
98
\newcommand{\convert}[5]{\mbox{$#1,#2 \these #3 =_{#4}#5 $}}
 
99
\newcommand{\convorder}[5]{\mbox{$#1,#2 \these #3\leq _{#4}#5 $}}
 
100
\newcommand{\wouff}[2]{\mbox{$\emph{WF}(#1)[#2]$}}
 
101
 
 
102
 
 
103
%\newcommand{\mthese}{\underset{M}{\vdash}}
 
104
\newcommand{\mthese}{\boldsymbol{\vdash}_{\!\!M}}
 
105
\newcommand{\type}{\boldsymbol{:}}
 
106
 
 
107
% jugement absolu
 
108
 
 
109
%\newcommand{\ajuge}[2]{\mbox{$ \boldsymbol{\vdash} #1 : #2 $}}
 
110
\newcommand{\ajuge}[2]{\mbox{$\these #1 \boldsymbol{:} #2 $}}
 
111
 
 
112
%%% logique minimale
 
113
\newcommand{\propzero}{\mbox{$P_0$}} % types de Fzero
 
114
 
 
115
%%% logique propositionnelle classique
 
116
\newcommand {\ff}{\boldsymbol{f}} % faux
 
117
\newcommand {\vv}{\boldsymbol{t}} % vrai
 
118
 
 
119
\newcommand{\verite}{\mbox{$\cal{B}$}} % {\ff,\vv}
 
120
\newcommand{\sequ}[2]{\mbox{$#1 \vdash #2 $}} % sequent
 
121
\newcommand{\strip}[1]{#1^o} % enlever les variables d'un contexte
 
122
 
 
123
 
 
124
 
 
125
%%% tactiques
 
126
\newcommand{\decomp}{\delta} % decomposition
 
127
\newcommand{\recomp}{\rho} % recomposition
 
128
 
 
129
%%% divers
 
130
\newcommand{\cqfd}{\mbox{\textbf{cqfd}}}
 
131
\newcommand{\fail}{\mbox{\textbf{F}}}
 
132
\newcommand{\succes}{\mbox{$\blacksquare$}}
 
133
%%% Environnements
 
134
 
 
135
 
 
136
%% Fzero
 
137
\newcommand{\con}{\mbox{$\cal C$}}
 
138
\newcommand{\var}{\mbox{$\cal V$}}
 
139
 
 
140
\newcommand{\atomzero}{\mbox{${\cal A}_0$}} % types de base de Fzero
 
141
\newcommand{\typezero}{\mbox{${\cal T}_0$}} % types de Fzero
 
142
\newcommand{\termzero}{\mbox{$\Lambda_0$}} % termes de Fzero 
 
143
\newcommand{\conzero}{\mbox{$\cal C_0$}} % contextes de Fzero 
 
144
 
 
145
\newcommand{\buts}{\mbox{$\cal B$}} % buts
 
146
 
 
147
%%% for drawing terms
 
148
% abstraction [x:t]e
 
149
\newcommand{\PicAbst}[3]{\begin{bundle}{\bf abst}\chunk{#1}\chunk{#2}\chunk{#3}%
 
150
                        \end{bundle}}
 
151
 
 
152
% the same in DeBruijn form
 
153
\newcommand{\PicDbj}[2]{\begin{bundle}{\bf abst}\chunk{#1}\chunk{#2}
 
154
                       \end{bundle}}
 
155
 
 
156
 
 
157
% applications
 
158
\newcommand{\PicAppl}[2]{\begin{bundle}{\bf appl}\chunk{#1}\chunk{#2}%
 
159
                         \end{bundle}}
 
160
 
 
161
% variables
 
162
\newcommand{\PicVar}[1]{\begin{bundle}{\bf var}\chunk{#1}
 
163
                          \end{bundle}}
 
164
 
 
165
% constantes
 
166
\newcommand{\PicCon}[1]{\begin{bundle}{\bf const}\chunk{#1}\end{bundle}}
 
167
 
 
168
% arrows
 
169
\newcommand{\PicImpl}[2]{\begin{bundle}{\impl}\chunk{#1}\chunk{#2}%
 
170
                         \end{bundle}}
 
171
 
 
172
 
 
173
 
 
174
%%%% scripts coq
 
175
\newcommand{\prompt}{\mbox{\sl Coq $<\;$}}
 
176
\newcommand{\natquicksort}{\texttt{nat\_quicksort}}
 
177
\newcommand{\citecoq}[1]{\mbox{\texttt{#1}}}
 
178
\newcommand{\safeit}{\it}
 
179
\newtheorem{remarque}{Remark}[section]
 
180
%\newtheorem{definition}{Definition}[chapter]