← Back to branch summary

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

« back to all changes in this revision

Viewing changes to 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:
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]